Theorem ad3antrrr 483

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 479	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  485  ad5ant12  509  disjiun  3924  tfr1onlemaccex  6245  tfrcllemaccex  6258  phplem4on  6761  dif1enen  6774  en2eqpr  6801  unsnfidcex  6808  unsnfidcel  6809  unfidisj  6810  undifdc  6812  fiintim  6817  ssfirab  6822  suplub2ti  6888  djudom  6978  omp1eomlem  6979  difinfsnlem  6984  difinfinf  6986  ctssdclemn0  6995  ctssdc  6998  ltaddpr  7405  ltexprlemrl  7418  addcanprleml  7422  addcanprlemu  7423  aptiprleml  7447  aptiprlemu  7448  cauappcvgprlemdisj  7459  cauappcvgprlemladdrl  7465  caucvgprlemloc  7483  caucvgprlemladdrl  7486  caucvgprprlemopl  7505  caucvgprprlemloc  7511  caucvgprprlemexbt  7514  suplocexprlemrl  7525  suplocexprlemru  7527  suplocexprlemdisj  7528  suplocexprlemloc  7529  suplocexprlemub  7531  caucvgsrlemoffres  7608  suplocsrlem  7616  axcaucvglemcau  7706  axcaucvglemres  7707  negf1o  8144  apreim  8365  apsym  8368  apcotr  8369  apadd1  8370  apneg  8373  mulext1  8374  mulge0  8381  apti  8384  aprcl  8408  qapne  9431  xaddf  9627  xaddval  9628  qtri3or  10020  exbtwnzlemstep  10025  rebtwn2zlemstep  10030  addmodlteq  10171  seq3f1olemqsumk  10272  seq3f1oleml  10276  faclbnd  10487  hashennnuni  10525  cvg1nlemres  10757  resqrexlemoverl  10793  resqrexlemglsq  10794  resqrexlemga  10795  minmax  11001  xrmaxleim  11013  xrmaxifle  11015  xrmaxiflemab  11016  xrmaxiflemlub  11017  xrmaxiflemcom  11018  xrmaxltsup  11027  xrmaxadd  11030  xrminmax  11034  xrbdtri  11045  climrecvg1n  11117  serf0  11121  zsumdc  11153  isumss  11160  fisumss  11161  fsum3cvg3  11165  fsumcl2lem  11167  fsumadd  11175  fsummulc2  11217  divcnv  11266  cvgratz  11301  mertenslem2  11305  dvds2ln  11526  divalglemeunn  11618  divalglemeuneg  11620  zsupcllemstep  11638  dvdsbnd  11645  bezoutlemnewy  11684  bezoutlemstep  11685  bezoutlemmain  11686  bezoutlembi  11693  dfgcd3  11698  lcmgcdlem  11758  cncongr1  11784  cncongr2  11785  ennnfonelemhom  11928  ennnfonelemrnh  11929  ctinfomlemom  11940  cnpnei  12388  cnntr  12394  cncnp  12399  lmtopcnp  12419  txdis1cn  12447  xmettxlem  12678  metcnp3  12680  fsumcncntop  12725  cncfco  12747  mulcncf  12760  dedekindeulemuub  12764  dedekindeulemlu  12768  dedekindicclemuub  12773  dedekindicclemlu  12777  dedekindicclemicc  12779  ivthinclemlr  12784  ivthinclemur  12786  limcimo  12803  cnplimcim  12805  pilem3  12864  peano4nninf  13200  trilpolemeq1  13233