Theorem ad3antrrr 475

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

Hypothesis

Ref	Expression
ad2ant.1	⊢ (𝜑 → 𝜓)

Assertion

Ref	Expression
ad3antrrr	⊢ ((((𝜑 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) → 𝜓)

Proof of Theorem ad3antrrr

Step	Hyp	Ref	Expression
1		ad2ant.1	. . 3 ⊢ (𝜑 → 𝜓)
2	1	adantr 270	. 2 ⊢ ((𝜑 ∧ 𝜒) → 𝜓)
3	2	ad2antrr 471	1 ⊢ ((((𝜑 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 102

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

This theorem is referenced by:  ad4antr  477  phplem4on  6353  en2eqpr  6380  unsnfidcex  6385  unsnfidcel  6386  suplub2ti  6414  ltaddpr  6787  ltexprlemrl  6800  addcanprleml  6804  addcanprlemu  6805  aptiprleml  6829  aptiprlemu  6830  cauappcvgprlemdisj  6841  cauappcvgprlemladdrl  6847  caucvgprlemloc  6865  caucvgprlemladdrl  6868  caucvgprprlemopl  6887  caucvgprprlemloc  6893  caucvgprprlemexbt  6896  caucvgsrlemoffres  6976  axcaucvglemcau  7064  axcaucvglemres  7065  negf1o  7486  apreim  7703  apsym  7706  apcotr  7707  apadd1  7708  apneg  7711  mulext1  7712  mulge0  7719  apti  7722  qapne  8724  qtri3or  9252  qbtwnzlemstep  9257  rebtwn2zlemstep  9261  addmodlteq  9400  faclbnd  9668  cvg1nlemres  9871  resqrexlemoverl  9907  resqrexlemglsq  9908  resqrexlemga  9909  minmax  10112  climrecvg1n  10185  serif0  10189  dvds2ln  10228  divalglemeunn  10321  divalglemeuneg  10323  zsupcllemstep  10341  dvdsbnd  10348  bezoutlemnewy  10385  bezoutlemstep  10386  bezoutlemmain  10387  bezoutlembi  10394  dfgcd3  10399  lcmgcdlem  10459  cncongr1  10485  cncongr2  10486