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  960  prneimg  3775  f1oprg  5506  fvco4  5589  nnsucuniel  6496  mapen  6846  mapxpen  6848  fidceq  6869  fidifsnen  6870  php5fin  6882  findcard2d  6891  findcard2sd  6892  diffisn  6893  fidcenumlemr  6954  supmoti  6992  djuf1olem  7052  nninfwlpor  7172  exmidfodomrlemim  7200  cc4f  7268  cc4n  7270  subhalfnqq  7413  nqnq0pi  7437  genprndl  7520  genprndu  7521  addlocpr  7535  nqprl  7550  nqpru  7551  addnqprlemrl  7556  addnqprlemru  7557  mullocpr  7570  mulnqprlemrl  7572  mulnqprlemru  7573  ltaprlem  7617  aptiprleml  7638  cauappcvgprlemladdfu  7653  cauappcvgprlemladdfl  7654  caucvgprlemladdfu  7676  caucvgprprlemloc  7702  suplocexprlemrl  7716  suplocexprlemru  7718  mulcmpblnrlemg  7739  recexgt0sr  7772  pitonn  7847  rereceu  7888  rimul  8542  receuap  8626  peano5uzti  9361  iooshf  9952  seq3fveq2  10469  seq3id2  10509  seqfeq3  10512  expcl2lemap  10532  mulexpzap  10560  expnlbnd2  10646  hashfacen  10816  absexpzap  11089  fsumf1o  11398  fisum0diag2  11455  fsummulc2  11456  fprodmul  11599  fprodrev  11627  moddvds  11806  dvdsflip  11857  dfgcd3  12011  dfgcd2  12015  lcmgcdlem  12077  cncongr1  12103  hashgcdlem  12238  phisum  12240  pcval  12296  pcqcl  12306  pcid  12323  pcneg  12324  prmpwdvds  12353  pockthg  12355  4sqlem2  12387  setscom  12502  qusval  12744  mulgdirlem  13014  mulgass  13020  0nsg  13074  islmodd  13383  lmodvsmmulgdi  13413  tgcl  13567  epttop  13593  cnpnei  13722  txcn  13778  txdis1cn  13781  imasnopn  13802  hmeoimaf1o  13817  txhmeo  13822  metss2lem  14000  bdxmet  14004  bdmopn  14007  metrest  14009  xmetxp  14010  metcnp  14015  rprelogbmul  14376  logbgcd1irr  14388  lgseisenlem2  14454