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  3976  tfr1onlemaccex  6312  tfrcllemaccex  6325  phplem4on  6829  dif1enen  6842  en2eqpr  6869  unsnfidcex  6881  unsnfidcel  6882  unfidisj  6883  undifdc  6885  fiintim  6890  ssfirab  6895  suplub2ti  6962  djudom  7054  omp1eomlem  7055  difinfsnlem  7060  difinfinf  7062  ctssdclemn0  7071  ctssdc  7074  nnnninfeq2  7089  nninfisol  7093  cc3  7205  ltaddpr  7534  ltexprlemrl  7547  addcanprleml  7551  addcanprlemu  7552  aptiprleml  7576  aptiprlemu  7577  cauappcvgprlemdisj  7588  cauappcvgprlemladdrl  7594  caucvgprlemloc  7612  caucvgprlemladdrl  7615  caucvgprprlemopl  7634  caucvgprprlemloc  7640  caucvgprprlemexbt  7643  suplocexprlemrl  7654  suplocexprlemru  7656  suplocexprlemdisj  7657  suplocexprlemloc  7658  suplocexprlemub  7660  caucvgsrlemoffres  7737  suplocsrlem  7745  axcaucvglemcau  7835  axcaucvglemres  7836  negf1o  8276  apreim  8497  apsym  8500  apcotr  8501  apadd1  8502  apneg  8505  mulext1  8506  mulge0  8513  apti  8516  aprcl  8540  qapne  9573  xaddf  9776  xaddval  9777  qtri3or  10174  exbtwnzlemstep  10179  rebtwn2zlemstep  10184  addmodlteq  10329  seq3f1olemqsumk  10430  seq3f1oleml  10434  qsqeqor  10561  apexp1  10627  faclbnd  10650  hashennnuni  10688  cvg1nlemres  10923  resqrexlemoverl  10959  resqrexlemglsq  10960  resqrexlemga  10961  minmax  11167  xrmaxleim  11181  xrmaxifle  11183  xrmaxiflemab  11184  xrmaxiflemlub  11185  xrmaxiflemcom  11186  xrmaxltsup  11195  xrmaxadd  11198  xrminmax  11202  xrbdtri  11213  climrecvg1n  11285  serf0  11289  zsumdc  11321  isumss  11328  fisumss  11329  fsum3cvg3  11333  fsumcl2lem  11335  fsumadd  11343  fsummulc2  11385  divcnv  11434  cvgratz  11469  mertenslem2  11473  zproddc  11516  fprodssdc  11527  fprodmul  11528  fprodsplitdc  11533  fprodcl2lem  11542  fprodle  11577  fprodmodd  11578  p1modz1  11730  dvds2ln  11760  divalglemeunn  11854  divalglemeuneg  11856  zsupcllemstep  11874  dvdsbnd  11885  bezoutlemnewy  11925  bezoutlemstep  11926  bezoutlemmain  11927  bezoutlembi  11934  dfgcd3  11939  uzwodc  11966  lcmgcdlem  12005  cncongr1  12031  cncongr2  12032  isprm5  12070  odzdvds  12173  pclemdc  12216  pceu  12223  dvdsprmpweqle  12264  pcadd  12267  1arith  12293  ennnfonelemhom  12344  ennnfonelemrnh  12345  ctinfomlemom  12356  cnpnei  12819  cnntr  12825  cncnp  12830  lmtopcnp  12850  txdis1cn  12878  xmettxlem  13109  metcnp3  13111  fsumcncntop  13156  cncfco  13178  mulcncf  13191  dedekindeulemuub  13195  dedekindeulemlu  13199  dedekindicclemuub  13204  dedekindicclemlu  13208  dedekindicclemicc  13210  ivthinclemlr  13215  ivthinclemur  13217  limcimo  13234  cnplimcim  13236  pilem3  13304  lgsfcl2  13507  lgsval2lem  13511  lgsdir  13536  lgsne0  13539  peano4nninf  13846  trilpolemeq1  13879