Theorem ad2antll 483

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

Syntax hints:   -> wi 4   /\ wa 103

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

This theorem is referenced by:  simprr  522  simprrl  529  simprrr  530  dn1dc  945  prneimg  3709  f1oprg  5419  fvco4  5501  nnsucuniel  6399  mapen  6748  mapxpen  6750  fidceq  6771  fidifsnen  6772  php5fin  6784  findcard2d  6793  findcard2sd  6794  diffisn  6795  fidcenumlemr  6851  supmoti  6888  djuf1olem  6946  exmidfodomrlemim  7074  cc4f  7101  cc4n  7103  subhalfnqq  7246  nqnq0pi  7270  genprndl  7353  genprndu  7354  addlocpr  7368  nqprl  7383  nqpru  7384  addnqprlemrl  7389  addnqprlemru  7390  mullocpr  7403  mulnqprlemrl  7405  mulnqprlemru  7406  ltaprlem  7450  aptiprleml  7471  cauappcvgprlemladdfu  7486  cauappcvgprlemladdfl  7487  caucvgprlemladdfu  7509  caucvgprprlemloc  7535  suplocexprlemrl  7549  suplocexprlemru  7551  mulcmpblnrlemg  7572  recexgt0sr  7605  pitonn  7680  rereceu  7721  rimul  8371  receuap  8454  peano5uzti  9183  iooshf  9765  seq3fveq2  10273  seq3id2  10313  seqfeq3  10316  expcl2lemap  10336  mulexpzap  10364  expnlbnd2  10448  hashfacen  10611  absexpzap  10884  fsumf1o  11191  fisum0diag2  11248  fsummulc2  11249  moddvds  11538  dvdsflip  11585  dfgcd3  11734  dfgcd2  11738  lcmgcdlem  11794  cncongr1  11820  hashgcdlem  11939  setscom  12038  tgcl  12272  epttop  12298  cnpnei  12427  txcn  12483  txdis1cn  12486  imasnopn  12507  hmeoimaf1o  12522  txhmeo  12527  metss2lem  12705  bdxmet  12709  bdmopn  12712  metrest  12714  xmetxp  12715  metcnp  12720  rprelogbmul  13080  logbgcd1irr  13092