Theorem ad3antrrr 477

Description: Deduction adding three conjuncts to antecedent. (Contributed by NM, 28-Jul-2012.)

Hypothesis

Ref	Expression
ad2ant.1	|- ( ph -> ps )

Assertion

Ref	Expression
ad3antrrr	|- ( ( ( ( ph /\ ch ) /\ th ) /\ ta ) -> ps )

Proof of Theorem ad3antrrr

Step	Hyp	Ref	Expression
1		ad2ant.1	. . 3 |- ( ph -> ps )
2	1	adantr 271	. 2 |- ( ( ph /\ ch ) -> ps )
3	2	ad2antrr 473	1 |- ( ( ( ( ph /\ ch ) /\ th ) /\ ta ) -> ps )

Syntax hints:   -> wi 4   /\ wa 103

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

This theorem is referenced by:  ad4antr  479  disjiun  3846  tfr1onlemaccex  6127  tfrcllemaccex  6140  phplem4on  6637  dif1enen  6650  en2eqpr  6677  unsnfidcex  6684  unsnfidcel  6685  unfidisj  6686  undifdc  6688  fiintim  6693  ssfirab  6697  suplub2ti  6750  djudom  6837  ltaddpr  7217  ltexprlemrl  7230  addcanprleml  7234  addcanprlemu  7235  aptiprleml  7259  aptiprlemu  7260  cauappcvgprlemdisj  7271  cauappcvgprlemladdrl  7277  caucvgprlemloc  7295  caucvgprlemladdrl  7298  caucvgprprlemopl  7317  caucvgprprlemloc  7323  caucvgprprlemexbt  7326  caucvgsrlemoffres  7406  axcaucvglemcau  7494  axcaucvglemres  7495  negf1o  7921  apreim  8141  apsym  8144  apcotr  8145  apadd1  8146  apneg  8149  mulext1  8150  mulge0  8157  apti  8160  qapne  9185  qtri3or  9715  exbtwnzlemstep  9720  rebtwn2zlemstep  9725  addmodlteq  9866  seq3f1olemqsumk  9989  seq3f1oleml  9993  faclbnd  10210  hashennnuni  10248  cvg1nlemres  10479  resqrexlemoverl  10515  resqrexlemglsq  10516  resqrexlemga  10517  minmax  10722  climrecvg1n  10798  serf0  10802  zisum  10835  isumss  10844  fisumss  10845  fsum3cvg3  10850  fsumcl2lem  10853  fsumadd  10861  fsummulc2  10903  divcnv  10952  cvgratz  10987  mertenslem2  10991  dvds2ln  11168  divalglemeunn  11260  divalglemeuneg  11262  zsupcllemstep  11280  dvdsbnd  11287  bezoutlemnewy  11324  bezoutlemstep  11325  bezoutlemmain  11326  bezoutlembi  11333  dfgcd3  11338  lcmgcdlem  11398  cncongr1  11424  cncongr2  11425  cncfco  11920  peano4nninf  12168