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  4081  tfr1onlemaccex  6509  tfrcllemaccex  6522  phplem4on  7049  dif1enen  7064  elssdc  7089  en2eqpr  7094  unsnfidcex  7107  unsnfidcel  7108  unfidisj  7109  undifdc  7111  fiintim  7118  ssfirab  7123  suplub2ti  7194  djudom  7286  omp1eomlem  7287  difinfsnlem  7292  difinfinf  7294  ctssdclemn0  7303  ctssdc  7306  nnnninfeq2  7322  nninfisol  7326  nninfwlpoimlemginf  7369  cc3  7480  ltaddpr  7810  ltexprlemrl  7823  addcanprleml  7827  addcanprlemu  7828  aptiprleml  7852  aptiprlemu  7853  cauappcvgprlemdisj  7864  cauappcvgprlemladdrl  7870  caucvgprlemloc  7888  caucvgprlemladdrl  7891  caucvgprprlemopl  7910  caucvgprprlemloc  7916  caucvgprprlemexbt  7919  suplocexprlemrl  7930  suplocexprlemru  7932  suplocexprlemdisj  7933  suplocexprlemloc  7934  suplocexprlemub  7936  caucvgsrlemoffres  8013  suplocsrlem  8021  axcaucvglemcau  8111  axcaucvglemres  8112  negf1o  8554  apreim  8776  apsym  8779  apcotr  8780  apadd1  8781  apneg  8784  mulext1  8785  mulge0  8792  apti  8795  aprcl  8819  qapne  9866  xaddf  10072  xaddval  10073  zsupcllemstep  10482  qtri3or  10493  exbtwnzlemstep  10500  rebtwn2zlemstep  10505  addmodlteq  10653  seq3f1olemqsumk  10767  seq3f1oleml  10771  qsqeqor  10905  apexp1  10973  faclbnd  10996  hashennnuni  11034  swrdswrd  11279  swrdccatin1  11299  pfxccatin12lem3  11306  swrdccat3blem  11313  cvg1nlemres  11539  resqrexlemoverl  11575  resqrexlemglsq  11576  resqrexlemga  11577  minmax  11784  xrmaxleim  11798  xrmaxifle  11800  xrmaxiflemab  11801  xrmaxiflemlub  11802  xrmaxiflemcom  11803  xrmaxltsup  11812  xrmaxadd  11815  xrminmax  11819  xrbdtri  11830  climrecvg1n  11902  serf0  11906  zsumdc  11938  isumss  11945  fisumss  11946  fsum3cvg3  11950  fsumcl2lem  11952  fsumadd  11960  fsummulc2  12002  divcnv  12051  cvgratz  12086  mertenslem2  12090  zproddc  12133  fprodssdc  12144  fprodmul  12145  fprodsplitdc  12150  fprodcl2lem  12159  fprodle  12194  fprodmodd  12195  p1modz1  12348  dvds2ln  12378  divalglemeunn  12475  divalglemeuneg  12477  bitsfzolem  12508  dvdsbnd  12520  bezoutlemnewy  12560  bezoutlemstep  12561  bezoutlemmain  12562  bezoutlembi  12569  dfgcd3  12574  uzwodc  12601  nninfctlemfo  12604  lcmgcdlem  12642  cncongr1  12668  cncongr2  12669  isprm5  12707  odzdvds  12811  pclemdc  12854  pceu  12861  dvdsprmpweqle  12903  pcadd  12906  1arith  12933  4sqexercise2  12965  4sqlem13m  12969  ennnfonelemhom  13029  ennnfonelemrnh  13030  ctinfomlemom  13041  prdsval  13349  resmhm2b  13565  mhmid  13695  mhmmnd  13696  ghmgrp  13698  mulgfng  13704  conjnmzb  13860  imasabl  13916  issrg  13971  ringinvnzdiv  14056  znunit  14666  psrval  14673  mplsubgfilemcl  14706  cnpnei  14936  cnntr  14942  cncnp  14947  lmtopcnp  14967  txdis1cn  14995  xmettxlem  15226  metcnp3  15228  fsumcncntop  15284  cncfco  15308  mulcncf  15325  dedekindeulemuub  15334  dedekindeulemlu  15338  dedekindicclemuub  15343  dedekindicclemlu  15347  dedekindicclemicc  15349  ivthinclemlr  15354  ivthinclemur  15356  limcimo  15382  cnplimcim  15384  plymullem1  15465  plycolemc  15475  plycj  15478  dvply2g  15483  pilem3  15500  lgsfcl2  15728  lgsval2lem  15732  lgsdir  15757  lgsne0  15760  gausslemma2dlem1a  15780  gausslemma2dlem1f1o  15782  lgsquad3  15806  umgrvad2edg  16055  usgredg2vlem2  16067  wlkvtxiedg  16156  wlkvtxiedgg  16157  clwwlkccatlem  16209  peano4nninf  16558  nnnninfex  16574  trilpolemeq1  16594  gfsumval  16630