Theorem ad2antll 495

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 )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem is used by:  simprr  537  simprrl  545  simprrr  546  dn1dc  973  prneimg  3899  f1oprg  5685  fvco4  5777  nnsucuniel  6768  modom  7108  mapen  7146  mapxpen  7148  mapunen  7151  fidceq  7171  fidifsnen  7172  php5fin  7186  findcard2d  7195  findcard2sd  7196  diffisn  7197  fidcenumlemr  7272  supmoti  7333  djuf1olem  7393  nninfwlpor  7514  exmidfodomrlemim  7553  cc4f  7635  cc4n  7637  subhalfnqq  7781  nqnq0pi  7805  genprndl  7888  genprndu  7889  addlocpr  7903  nqprl  7918  nqpru  7919  addnqprlemrl  7924  addnqprlemru  7925  mullocpr  7938  mulnqprlemrl  7940  mulnqprlemru  7941  ltaprlem  7985  aptiprleml  8006  cauappcvgprlemladdfu  8021  cauappcvgprlemladdfl  8022  caucvgprlemladdfu  8044  caucvgprprlemloc  8070  suplocexprlemrl  8084  suplocexprlemru  8086  mulcmpblnrlemg  8107  recexgt0sr  8140  pitonn  8215  rereceu  8256  rimul  8913  receuap  8999  peano5uzti  9754  iooshf  10354  seq3fveq2  10912  seqfveq2g  10914  seq3id2  10963  seqfeq3  10966  expcl2lemap  10988  mulexpzap  11016  expnlbnd2  11103  hashfacen  11284  hashf1lem1  11285  fstwrdne0  11344  swrdsb0eq  11437  swrdswrd  11477  wrd2ind  11495  swrdccatin1  11497  pfxccatin12  11505  pfxccat3  11506  swrdccat  11507  absexpzap  11846  fsumf1o  12157  fisum0diag2  12214  fsummulc2  12215  fprodmul  12358  fprodrev  12386  moddvds  12566  dvdsflip  12618  dfgcd3  12787  dfgcd2  12791  lcmgcdlem  12855  cncongr1  12881  hashgcdlem  13016  phisum  13019  pcval  13075  pcqcl  13085  pcid  13103  pcneg  13104  prmpwdvds  13134  pockthg  13136  4sqlem2  13168  4sqlem11  13180  ballotfilemsf1o  13257  setscom  13392  qusval  13644  mulgdirlem  13956  mulgass  13962  0nsg  14017  ghmmulg  14059  islmodd  14629  lmodvsmmulgdi  14660  islss3  14716  znf1o  14986  tgcl  15165  epttop  15191  cnpnei  15320  txcn  15376  txdis1cn  15379  imasnopn  15400  hmeoimaf1o  15415  txhmeo  15420  metss2lem  15598  bdxmet  15602  bdmopn  15605  metrest  15607  xmetxp  15608  metcnp  15613  dvmptfsum  15826  plycn  15863  dvply2g  15867  rprelogbmul  16057  logbgcd1irr  16069  mpodvdsmulf1o  16104  gausslemma2dlem1a  16177  lgseisenlem2  16190  lgsquadlemsfi  16194  lgsquadlem1  16196  lgsquadlem2  16197  lgsquadlem3  16198  subgrprop3  16503  subupgr  16514  wlkl1loop  16599  clwwlknp  16658