Theorem ad3antrrr 492

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

Syntax hints:   → wi 4   ∧ wa 104

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

This theorem is referenced by:  ad4antr  494  ad5ant12  518  disjiun  4106  tfr1onlemaccex  6581  tfrcllemaccex  6594  phplem4on  7124  dif1enen  7139  elssdc  7164  en2eqpr  7169  unsnfidcex  7182  unsnfidcel  7183  unfidisj  7184  undifdc  7186  fiintim  7193  ssfirab  7199  suplub2ti  7294  djudom  7386  omp1eomlem  7387  difinfsnlem  7392  difinfinf  7394  ctssdclemn0  7403  ctssdc  7406  nnnninfeq2  7422  nninfisol  7426  nninfwlpoimlemginf  7469  cc3  7587  ltaddpr  7917  ltexprlemrl  7930  addcanprleml  7934  addcanprlemu  7935  aptiprleml  7959  aptiprlemu  7960  cauappcvgprlemdisj  7971  cauappcvgprlemladdrl  7977  caucvgprlemloc  7995  caucvgprlemladdrl  7998  caucvgprprlemopl  8017  caucvgprprlemloc  8023  caucvgprprlemexbt  8026  suplocexprlemrl  8037  suplocexprlemru  8039  suplocexprlemdisj  8040  suplocexprlemloc  8041  suplocexprlemub  8043  caucvgsrlemoffres  8120  suplocsrlem  8128  axcaucvglemcau  8218  axcaucvglemres  8219  negf1o  8660  apreim  8882  apsym  8885  apcotr  8886  apadd1  8887  apneg  8890  mulext1  8891  mulge0  8898  apti  8901  aprcl  8925  qapne  9977  xaddf  10183  xaddval  10184  zsupcllemstep  10596  qtri3or  10607  exbtwnzlemstep  10614  rebtwn2zlemstep  10619  addmodlteq  10767  seq3f1olemqsumk  10881  seq3f1oleml  10885  qsqeqor  11019  apexp1  11088  faclbnd  11111  hashennnuni  11150  swrdswrd  11405  swrdccatin1  11425  pfxccatin12lem3  11432  swrdccat3blem  11439  cvg1nlemres  11678  resqrexlemoverl  11714  resqrexlemglsq  11715  resqrexlemga  11716  minmax  11923  xrmaxleim  11937  xrmaxifle  11939  xrmaxiflemab  11940  xrmaxiflemlub  11941  xrmaxiflemcom  11942  xrmaxltsup  11951  xrmaxadd  11954  xrminmax  11958  xrbdtri  11969  climrecvg1n  12041  serf0  12045  zsumdc  12078  isumss  12085  fisumss  12086  fsum3cvg3  12090  fsumcl2lem  12092  fsumadd  12100  fsummulc2  12142  divcnv  12191  cvgratz  12226  mertenslem2  12230  zproddc  12273  fprodssdc  12284  fprodmul  12285  fprodsplitdc  12290  fprodcl2lem  12299  fprodle  12334  fprodmodd  12335  p1modz1  12488  dvds2ln  12518  divalglemeunn  12615  divalglemeuneg  12617  bitsfzolem  12648  dvdsbnd  12660  bezoutlemnewy  12700  bezoutlemstep  12701  bezoutlemmain  12702  bezoutlembi  12709  dfgcd3  12714  uzwodc  12741  nninfctlemfo  12744  lcmgcdlem  12782  cncongr1  12808  cncongr2  12809  isprm5  12847  odzdvds  12951  pclemdc  12994  pceu  13001  dvdsprmpweqle  13043  pcadd  13046  1arith  13073  4sqexercise2  13105  4sqlem13m  13109  ballotfilemcdc  13150  ennnfonelemhom  13187  ennnfonelemrnh  13188  ctinfomlemom  13199  prdsval  13507  resmhm2b  13723  mhmid  13853  mhmmnd  13854  ghmgrp  13856  mulgfng  13862  conjnmzb  14018  imasabl  14074  issrg  14130  ringinvnzdiv  14215  znunit  14856  psrval  14863  mplsubgfilemcl  14903  cnpnei  15133  cnntr  15139  cncnp  15144  lmtopcnp  15164  txdis1cn  15192  xmettxlem  15423  metcnp3  15425  fsumcncntop  15481  cncfco  15505  mulcncf  15522  dedekindeulemuub  15531  dedekindeulemlu  15535  dedekindicclemuub  15540  dedekindicclemlu  15544  dedekindicclemicc  15546  ivthinclemlr  15551  ivthinclemur  15553  limcimo  15579  cnplimcim  15581  plymullem1  15662  plycolemc  15672  plycj  15675  dvply2g  15680  pilem3  15697  lgsfcl2  15928  lgsval2lem  15932  lgsdir  15957  lgsne0  15960  gausslemma2dlem1a  15980  gausslemma2dlem1f1o  15982  lgsquad3  16006  umgrvad2edg  16255  usgredg2vlem2  16267  wlkvtxiedg  16389  wlkvtxiedgg  16390  clwwlkccatlem  16444  eupth2lem3lem4fi  16517  eupth2lemsfi  16522  peano4nninf  16833  nnnninfex  16849  trilpolemeq1  16873  trimul0or  16894  gfsumval  16911  gfsumcl  16919