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  962  prneimg  3792  f1oprg  5527  fvco4  5612  nnsucuniel  6524  mapen  6878  mapxpen  6880  fidceq  6901  fidifsnen  6902  php5fin  6914  findcard2d  6923  findcard2sd  6924  diffisn  6925  fidcenumlemr  6988  supmoti  7026  djuf1olem  7086  nninfwlpor  7207  exmidfodomrlemim  7235  cc4f  7303  cc4n  7305  subhalfnqq  7448  nqnq0pi  7472  genprndl  7555  genprndu  7556  addlocpr  7570  nqprl  7585  nqpru  7586  addnqprlemrl  7591  addnqprlemru  7592  mullocpr  7605  mulnqprlemrl  7607  mulnqprlemru  7608  ltaprlem  7652  aptiprleml  7673  cauappcvgprlemladdfu  7688  cauappcvgprlemladdfl  7689  caucvgprlemladdfu  7711  caucvgprprlemloc  7737  suplocexprlemrl  7751  suplocexprlemru  7753  mulcmpblnrlemg  7774  recexgt0sr  7807  pitonn  7882  rereceu  7923  rimul  8577  receuap  8661  peano5uzti  9396  iooshf  9988  seq3fveq2  10508  seq3id2  10548  seqfeq3  10551  expcl2lemap  10572  mulexpzap  10600  expnlbnd2  10686  hashfacen  10857  absexpzap  11130  fsumf1o  11439  fisum0diag2  11496  fsummulc2  11497  fprodmul  11640  fprodrev  11668  moddvds  11847  dvdsflip  11898  dfgcd3  12052  dfgcd2  12056  lcmgcdlem  12120  cncongr1  12146  hashgcdlem  12281  phisum  12283  pcval  12339  pcqcl  12349  pcid  12367  pcneg  12368  prmpwdvds  12398  pockthg  12400  4sqlem2  12432  4sqlem11  12444  setscom  12563  qusval  12811  mulgdirlem  13118  mulgass  13124  0nsg  13178  ghmmulg  13220  islmodd  13634  lmodvsmmulgdi  13664  islss3  13720  tgcl  14049  epttop  14075  cnpnei  14204  txcn  14260  txdis1cn  14263  imasnopn  14284  hmeoimaf1o  14299  txhmeo  14304  metss2lem  14482  bdxmet  14486  bdmopn  14489  metrest  14491  xmetxp  14492  metcnp  14497  rprelogbmul  14858  logbgcd1irr  14870  lgseisenlem2  14937