Theorem ad3antrrr 477

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 271	. 2 ⊢ ((𝜑 ∧ 𝜒) → 𝜓)
3	2	ad2antrr 473	1 ⊢ ((((𝜑 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) → 𝜓)

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  3862  tfr1onlemaccex  6151  tfrcllemaccex  6164  phplem4on  6663  dif1enen  6676  en2eqpr  6703  unsnfidcex  6710  unsnfidcel  6711  unfidisj  6712  undifdc  6714  fiintim  6719  ssfirab  6723  suplub2ti  6776  djudom  6863  ltaddpr  7253  ltexprlemrl  7266  addcanprleml  7270  addcanprlemu  7271  aptiprleml  7295  aptiprlemu  7296  cauappcvgprlemdisj  7307  cauappcvgprlemladdrl  7313  caucvgprlemloc  7331  caucvgprlemladdrl  7334  caucvgprprlemopl  7353  caucvgprprlemloc  7359  caucvgprprlemexbt  7362  caucvgsrlemoffres  7442  axcaucvglemcau  7530  axcaucvglemres  7531  negf1o  7957  apreim  8177  apsym  8180  apcotr  8181  apadd1  8182  apneg  8185  mulext1  8186  mulge0  8193  apti  8196  qapne  9223  xaddf  9410  xaddval  9411  qtri3or  9803  exbtwnzlemstep  9808  rebtwn2zlemstep  9813  addmodlteq  9954  seq3f1olemqsumk  10049  seq3f1oleml  10053  faclbnd  10264  hashennnuni  10302  cvg1nlemres  10533  resqrexlemoverl  10569  resqrexlemglsq  10570  resqrexlemga  10571  minmax  10776  xrmaxleim  10787  xrmaxifle  10789  xrmaxiflemab  10790  xrmaxiflemlub  10791  xrmaxiflemcom  10792  xrmaxltsup  10801  xrmaxadd  10804  xrminmax  10808  xrbdtri  10819  climrecvg1n  10891  serf0  10895  zsumdc  10927  isumss  10934  fisumss  10935  fsum3cvg3  10939  fsumcl2lem  10941  fsumadd  10949  fsummulc2  10991  divcnv  11040  cvgratz  11075  mertenslem2  11079  dvds2ln  11256  divalglemeunn  11348  divalglemeuneg  11350  zsupcllemstep  11368  dvdsbnd  11375  bezoutlemnewy  11412  bezoutlemstep  11413  bezoutlemmain  11414  bezoutlembi  11421  dfgcd3  11426  lcmgcdlem  11486  cncongr1  11512  cncongr2  11513  cnpnei  12070  cnntr  12076  cncnp  12081  lmtopcnp  12101  metcnp3  12293  cncfco  12344  mulcncf  12354  peano4nninf  12601