Theorem ad2antll 407

Description: Deduction adding conjuncts to antecedent.

Hypothesis

Ref	Expression
ad2ant.1	|- (ph -> ps)

Assertion

Ref	Expression
ad2antll	|- ((ch /\ (th /\ ph)) -> ps)

Proof of Theorem ad2antll

Step	Hyp	Ref	Expression
1		ad2ant.1	. . 3 |- (ph -> ps)
2	1	adantl 388	. 2 |- ((th /\ ph) -> ps)
3	2	adantl 388	1 |- ((ch /\ (th /\ ph)) -> ps)

Syntax hints:   -> wi 3   /\ wa 223

This theorem is referenced by:  simprr 415  ax11eq 1363  ax11el 1364  ordsucelsuc 3073  funfvima3 3854  isomin 3899  oalimcl 4194  odi 4210  pw2en 4444  rankxplim3 4706  axacndlem5 4955  axacnd 4956  uzwo4OLD 6198  uzwo 6441  uzwoOLD 6442  recexpt 6581  replimt 6747  climaddlem3 7101  climmullem4 7108  fsum0diaglem2 7242  tgclt 7609  tgss2t 7622  neindisj 7716  dnsconst 7773  opni3 7851  lmcau 7981  grpidinvlem1 8033  grprcan 8048  sspval 8367  ubthlem3 8516  ubthlem4 8517  ubthlem12 8525  minveclem31 8560  minveclem32 8561  chocuni 9157  shscl 9266  spansneleq 9478  pjspansnt 9485  osumlem7 9569  3oalem2 9593  eigpos 9747  cnlnadjlem2 9986  stles 10153  mdslmd1lem1 10237  mdslmd1lem2 10238  cdj1 10345  trnij 10580  codcmpd 10623  cmpidb 10651  imonclem 10682  cmpmon 10684

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7

This theorem depends on definitions:  df-bi 147  df-an 225

Copyright terms: Public domain