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  4103  tfr1onlemaccex  6578  tfrcllemaccex  6591  phplem4on  7121  dif1enen  7136  elssdc  7161  en2eqpr  7166  unsnfidcex  7179  unsnfidcel  7180  unfidisj  7181  undifdc  7183  fiintim  7190  ssfirab  7196  suplub2ti  7291  djudom  7383  omp1eomlem  7384  difinfsnlem  7389  difinfinf  7391  ctssdclemn0  7400  ctssdc  7403  nnnninfeq2  7419  nninfisol  7423  nninfwlpoimlemginf  7466  cc3  7578  ltaddpr  7908  ltexprlemrl  7921  addcanprleml  7925  addcanprlemu  7926  aptiprleml  7950  aptiprlemu  7951  cauappcvgprlemdisj  7962  cauappcvgprlemladdrl  7968  caucvgprlemloc  7986  caucvgprlemladdrl  7989  caucvgprprlemopl  8008  caucvgprprlemloc  8014  caucvgprprlemexbt  8017  suplocexprlemrl  8028  suplocexprlemru  8030  suplocexprlemdisj  8031  suplocexprlemloc  8032  suplocexprlemub  8034  caucvgsrlemoffres  8111  suplocsrlem  8119  axcaucvglemcau  8209  axcaucvglemres  8210  negf1o  8651  apreim  8873  apsym  8876  apcotr  8877  apadd1  8878  apneg  8881  mulext1  8882  mulge0  8889  apti  8892  aprcl  8916  qapne  9967  xaddf  10173  xaddval  10174  zsupcllemstep  10585  qtri3or  10596  exbtwnzlemstep  10603  rebtwn2zlemstep  10608  addmodlteq  10756  seq3f1olemqsumk  10870  seq3f1oleml  10874  qsqeqor  11008  apexp1  11076  faclbnd  11099  hashennnuni  11137  swrdswrd  11390  swrdccatin1  11410  pfxccatin12lem3  11417  swrdccat3blem  11424  cvg1nlemres  11663  resqrexlemoverl  11699  resqrexlemglsq  11700  resqrexlemga  11701  minmax  11908  xrmaxleim  11922  xrmaxifle  11924  xrmaxiflemab  11925  xrmaxiflemlub  11926  xrmaxiflemcom  11927  xrmaxltsup  11936  xrmaxadd  11939  xrminmax  11943  xrbdtri  11954  climrecvg1n  12026  serf0  12030  zsumdc  12063  isumss  12070  fisumss  12071  fsum3cvg3  12075  fsumcl2lem  12077  fsumadd  12085  fsummulc2  12127  divcnv  12176  cvgratz  12211  mertenslem2  12215  zproddc  12258  fprodssdc  12269  fprodmul  12270  fprodsplitdc  12275  fprodcl2lem  12284  fprodle  12319  fprodmodd  12320  p1modz1  12473  dvds2ln  12503  divalglemeunn  12600  divalglemeuneg  12602  bitsfzolem  12633  dvdsbnd  12645  bezoutlemnewy  12685  bezoutlemstep  12686  bezoutlemmain  12687  bezoutlembi  12694  dfgcd3  12699  uzwodc  12726  nninfctlemfo  12729  lcmgcdlem  12767  cncongr1  12793  cncongr2  12794  isprm5  12832  odzdvds  12936  pclemdc  12979  pceu  12986  dvdsprmpweqle  13028  pcadd  13031  1arith  13058  4sqexercise2  13090  4sqlem13m  13094  ennnfonelemhom  13155  ennnfonelemrnh  13156  ctinfomlemom  13167  prdsval  13475  resmhm2b  13691  mhmid  13821  mhmmnd  13822  ghmgrp  13824  mulgfng  13830  conjnmzb  13986  imasabl  14042  issrg  14098  ringinvnzdiv  14183  znunit  14794  psrval  14801  mplsubgfilemcl  14841  cnpnei  15071  cnntr  15077  cncnp  15082  lmtopcnp  15102  txdis1cn  15130  xmettxlem  15361  metcnp3  15363  fsumcncntop  15419  cncfco  15443  mulcncf  15460  dedekindeulemuub  15469  dedekindeulemlu  15473  dedekindicclemuub  15478  dedekindicclemlu  15482  dedekindicclemicc  15484  ivthinclemlr  15489  ivthinclemur  15491  limcimo  15517  cnplimcim  15519  plymullem1  15600  plycolemc  15610  plycj  15613  dvply2g  15618  pilem3  15635  lgsfcl2  15866  lgsval2lem  15870  lgsdir  15895  lgsne0  15898  gausslemma2dlem1a  15918  gausslemma2dlem1f1o  15920  lgsquad3  15944  umgrvad2edg  16193  usgredg2vlem2  16205  wlkvtxiedg  16327  wlkvtxiedgg  16328  clwwlkccatlem  16382  eupth2lem3lem4fi  16455  eupth2lemsfi  16460  peano4nninf  16771  nnnninfex  16787  trilpolemeq1  16811  gfsumval  16848  gfsumcl  16856