Theorem ad2antll 491

Description: Deduction adding conjuncts to antecedent. (Contributed by NM, 19-Oct-1999.)

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 277	. 2 |- ( ( th /\ ph ) -> ps )
3	2	adantl 277	1 |- ( ( ch /\ ( th /\ ph ) ) -> ps )

Syntax hints:   -> wi 4   /\ wa 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem is referenced by:  simprr  531  simprrl  539  simprrr  540  dn1dc  966  prneimg  3852  f1oprg  5617  fvco4  5706  nnsucuniel  6641  mapen  7007  mapxpen  7009  fidceq  7031  fidifsnen  7032  php5fin  7044  findcard2d  7053  findcard2sd  7054  diffisn  7055  fidcenumlemr  7122  supmoti  7160  djuf1olem  7220  nninfwlpor  7341  exmidfodomrlemim  7379  cc4f  7455  cc4n  7457  subhalfnqq  7601  nqnq0pi  7625  genprndl  7708  genprndu  7709  addlocpr  7723  nqprl  7738  nqpru  7739  addnqprlemrl  7744  addnqprlemru  7745  mullocpr  7758  mulnqprlemrl  7760  mulnqprlemru  7761  ltaprlem  7805  aptiprleml  7826  cauappcvgprlemladdfu  7841  cauappcvgprlemladdfl  7842  caucvgprlemladdfu  7864  caucvgprprlemloc  7890  suplocexprlemrl  7904  suplocexprlemru  7906  mulcmpblnrlemg  7927  recexgt0sr  7960  pitonn  8035  rereceu  8076  rimul  8732  receuap  8816  peano5uzti  9555  iooshf  10148  seq3fveq2  10697  seqfveq2g  10699  seq3id2  10748  seqfeq3  10751  expcl2lemap  10773  mulexpzap  10801  expnlbnd2  10887  hashfacen  11058  fstwrdne0  11111  swrdsb0eq  11197  swrdswrd  11237  wrd2ind  11255  swrdccatin1  11257  pfxccatin12  11265  pfxccat3  11266  swrdccat  11267  absexpzap  11591  fsumf1o  11901  fisum0diag2  11958  fsummulc2  11959  fprodmul  12102  fprodrev  12130  moddvds  12310  dvdsflip  12362  dfgcd3  12531  dfgcd2  12535  lcmgcdlem  12599  cncongr1  12625  hashgcdlem  12760  phisum  12763  pcval  12819  pcqcl  12829  pcid  12847  pcneg  12848  prmpwdvds  12878  pockthg  12880  4sqlem2  12912  4sqlem11  12924  setscom  13072  qusval  13356  mulgdirlem  13690  mulgass  13696  0nsg  13751  ghmmulg  13793  islmodd  14257  lmodvsmmulgdi  14287  islss3  14343  znf1o  14615  tgcl  14738  epttop  14764  cnpnei  14893  txcn  14949  txdis1cn  14952  imasnopn  14973  hmeoimaf1o  14988  txhmeo  14993  metss2lem  15171  bdxmet  15175  bdmopn  15178  metrest  15180  xmetxp  15181  metcnp  15186  dvmptfsum  15399  plycn  15436  dvply2g  15440  rprelogbmul  15629  logbgcd1irr  15641  mpodvdsmulf1o  15664  gausslemma2dlem1a  15737  lgseisenlem2  15750  lgsquadlemsfi  15754  lgsquadlem1  15756  lgsquadlem2  15757  lgsquadlem3  15758  wlkl1loop  16069