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  533  simprrl  541  simprrr  542  dn1dc  969  prneimg  3862  f1oprg  5638  fvco4  5727  nnsucuniel  6706  modom  7037  mapen  7075  mapxpen  7077  fidceq  7099  fidifsnen  7100  php5fin  7114  findcard2d  7123  findcard2sd  7124  diffisn  7125  fidcenumlemr  7197  supmoti  7252  djuf1olem  7312  nninfwlpor  7433  exmidfodomrlemim  7472  cc4f  7548  cc4n  7550  subhalfnqq  7694  nqnq0pi  7718  genprndl  7801  genprndu  7802  addlocpr  7816  nqprl  7831  nqpru  7832  addnqprlemrl  7837  addnqprlemru  7838  mullocpr  7851  mulnqprlemrl  7853  mulnqprlemru  7854  ltaprlem  7898  aptiprleml  7919  cauappcvgprlemladdfu  7934  cauappcvgprlemladdfl  7935  caucvgprlemladdfu  7957  caucvgprprlemloc  7983  suplocexprlemrl  7997  suplocexprlemru  7999  mulcmpblnrlemg  8020  recexgt0sr  8053  pitonn  8128  rereceu  8169  rimul  8824  receuap  8908  peano5uzti  9649  iooshf  10248  seq3fveq2  10800  seqfveq2g  10802  seq3id2  10851  seqfeq3  10854  expcl2lemap  10876  mulexpzap  10904  expnlbnd2  10990  hashfacen  11163  fstwrdne0  11219  swrdsb0eq  11312  swrdswrd  11352  wrd2ind  11370  swrdccatin1  11372  pfxccatin12  11380  pfxccat3  11381  swrdccat  11382  absexpzap  11720  fsumf1o  12031  fisum0diag2  12088  fsummulc2  12089  fprodmul  12232  fprodrev  12260  moddvds  12440  dvdsflip  12492  dfgcd3  12661  dfgcd2  12665  lcmgcdlem  12729  cncongr1  12755  hashgcdlem  12890  phisum  12893  pcval  12949  pcqcl  12959  pcid  12977  pcneg  12978  prmpwdvds  13008  pockthg  13010  4sqlem2  13042  4sqlem11  13054  setscom  13202  qusval  13486  mulgdirlem  13820  mulgass  13826  0nsg  13881  ghmmulg  13923  islmodd  14389  lmodvsmmulgdi  14419  islss3  14475  znf1o  14747  tgcl  14875  epttop  14901  cnpnei  15030  txcn  15086  txdis1cn  15089  imasnopn  15110  hmeoimaf1o  15125  txhmeo  15130  metss2lem  15308  bdxmet  15312  bdmopn  15315  metrest  15317  xmetxp  15318  metcnp  15323  dvmptfsum  15536  plycn  15573  dvply2g  15577  rprelogbmul  15766  logbgcd1irr  15778  mpodvdsmulf1o  15804  gausslemma2dlem1a  15877  lgseisenlem2  15890  lgsquadlemsfi  15894  lgsquadlem1  15896  lgsquadlem2  15897  lgsquadlem3  15898  subgrprop3  16203  subupgr  16214  wlkl1loop  16299  clwwlknp  16358