Theorem ad3antrrr 484

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

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:  ad4antr  486  ad5ant12  510  disjiun  3932  tfr1onlemaccex  6253  tfrcllemaccex  6266  phplem4on  6769  dif1enen  6782  en2eqpr  6809  unsnfidcex  6816  unsnfidcel  6817  unfidisj  6818  undifdc  6820  fiintim  6825  ssfirab  6830  suplub2ti  6896  djudom  6986  omp1eomlem  6987  difinfsnlem  6992  difinfinf  6994  ctssdclemn0  7003  ctssdc  7006  cc3  7100  ltaddpr  7429  ltexprlemrl  7442  addcanprleml  7446  addcanprlemu  7447  aptiprleml  7471  aptiprlemu  7472  cauappcvgprlemdisj  7483  cauappcvgprlemladdrl  7489  caucvgprlemloc  7507  caucvgprlemladdrl  7510  caucvgprprlemopl  7529  caucvgprprlemloc  7535  caucvgprprlemexbt  7538  suplocexprlemrl  7549  suplocexprlemru  7551  suplocexprlemdisj  7552  suplocexprlemloc  7553  suplocexprlemub  7555  caucvgsrlemoffres  7632  suplocsrlem  7640  axcaucvglemcau  7730  axcaucvglemres  7731  negf1o  8168  apreim  8389  apsym  8392  apcotr  8393  apadd1  8394  apneg  8397  mulext1  8398  mulge0  8405  apti  8408  aprcl  8432  qapne  9458  xaddf  9657  xaddval  9658  qtri3or  10051  exbtwnzlemstep  10056  rebtwn2zlemstep  10061  addmodlteq  10202  seq3f1olemqsumk  10303  seq3f1oleml  10307  apexp1  10496  faclbnd  10519  hashennnuni  10557  cvg1nlemres  10789  resqrexlemoverl  10825  resqrexlemglsq  10826  resqrexlemga  10827  minmax  11033  xrmaxleim  11045  xrmaxifle  11047  xrmaxiflemab  11048  xrmaxiflemlub  11049  xrmaxiflemcom  11050  xrmaxltsup  11059  xrmaxadd  11062  xrminmax  11066  xrbdtri  11077  climrecvg1n  11149  serf0  11153  zsumdc  11185  isumss  11192  fisumss  11193  fsum3cvg3  11197  fsumcl2lem  11199  fsumadd  11207  fsummulc2  11249  divcnv  11298  cvgratz  11333  mertenslem2  11337  zproddc  11380  dvds2ln  11562  divalglemeunn  11654  divalglemeuneg  11656  zsupcllemstep  11674  dvdsbnd  11681  bezoutlemnewy  11720  bezoutlemstep  11721  bezoutlemmain  11722  bezoutlembi  11729  dfgcd3  11734  lcmgcdlem  11794  cncongr1  11820  cncongr2  11821  ennnfonelemhom  11964  ennnfonelemrnh  11965  ctinfomlemom  11976  cnpnei  12427  cnntr  12433  cncnp  12438  lmtopcnp  12458  txdis1cn  12486  xmettxlem  12717  metcnp3  12719  fsumcncntop  12764  cncfco  12786  mulcncf  12799  dedekindeulemuub  12803  dedekindeulemlu  12807  dedekindicclemuub  12812  dedekindicclemlu  12816  dedekindicclemicc  12818  ivthinclemlr  12823  ivthinclemur  12825  limcimo  12842  cnplimcim  12844  pilem3  12912  peano4nninf  13375  trilpolemeq1  13408