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  4083  tfr1onlemaccex  6514  tfrcllemaccex  6527  phplem4on  7054  dif1enen  7069  elssdc  7094  en2eqpr  7099  unsnfidcex  7112  unsnfidcel  7113  unfidisj  7114  undifdc  7116  fiintim  7123  ssfirab  7129  suplub2ti  7200  djudom  7292  omp1eomlem  7293  difinfsnlem  7298  difinfinf  7300  ctssdclemn0  7309  ctssdc  7312  nnnninfeq2  7328  nninfisol  7332  nninfwlpoimlemginf  7375  cc3  7487  ltaddpr  7817  ltexprlemrl  7830  addcanprleml  7834  addcanprlemu  7835  aptiprleml  7859  aptiprlemu  7860  cauappcvgprlemdisj  7871  cauappcvgprlemladdrl  7877  caucvgprlemloc  7895  caucvgprlemladdrl  7898  caucvgprprlemopl  7917  caucvgprprlemloc  7923  caucvgprprlemexbt  7926  suplocexprlemrl  7937  suplocexprlemru  7939  suplocexprlemdisj  7940  suplocexprlemloc  7941  suplocexprlemub  7943  caucvgsrlemoffres  8020  suplocsrlem  8028  axcaucvglemcau  8118  axcaucvglemres  8119  negf1o  8561  apreim  8783  apsym  8786  apcotr  8787  apadd1  8788  apneg  8791  mulext1  8792  mulge0  8799  apti  8802  aprcl  8826  qapne  9873  xaddf  10079  xaddval  10080  zsupcllemstep  10490  qtri3or  10501  exbtwnzlemstep  10508  rebtwn2zlemstep  10513  addmodlteq  10661  seq3f1olemqsumk  10775  seq3f1oleml  10779  qsqeqor  10913  apexp1  10981  faclbnd  11004  hashennnuni  11042  swrdswrd  11287  swrdccatin1  11307  pfxccatin12lem3  11314  swrdccat3blem  11321  cvg1nlemres  11547  resqrexlemoverl  11583  resqrexlemglsq  11584  resqrexlemga  11585  minmax  11792  xrmaxleim  11806  xrmaxifle  11808  xrmaxiflemab  11809  xrmaxiflemlub  11810  xrmaxiflemcom  11811  xrmaxltsup  11820  xrmaxadd  11823  xrminmax  11827  xrbdtri  11838  climrecvg1n  11910  serf0  11914  zsumdc  11947  isumss  11954  fisumss  11955  fsum3cvg3  11959  fsumcl2lem  11961  fsumadd  11969  fsummulc2  12011  divcnv  12060  cvgratz  12095  mertenslem2  12099  zproddc  12142  fprodssdc  12153  fprodmul  12154  fprodsplitdc  12159  fprodcl2lem  12168  fprodle  12203  fprodmodd  12204  p1modz1  12357  dvds2ln  12387  divalglemeunn  12484  divalglemeuneg  12486  bitsfzolem  12517  dvdsbnd  12529  bezoutlemnewy  12569  bezoutlemstep  12570  bezoutlemmain  12571  bezoutlembi  12578  dfgcd3  12583  uzwodc  12610  nninfctlemfo  12613  lcmgcdlem  12651  cncongr1  12677  cncongr2  12678  isprm5  12716  odzdvds  12820  pclemdc  12863  pceu  12870  dvdsprmpweqle  12912  pcadd  12915  1arith  12942  4sqexercise2  12974  4sqlem13m  12978  ennnfonelemhom  13038  ennnfonelemrnh  13039  ctinfomlemom  13050  prdsval  13358  resmhm2b  13574  mhmid  13704  mhmmnd  13705  ghmgrp  13707  mulgfng  13713  conjnmzb  13869  imasabl  13925  issrg  13981  ringinvnzdiv  14066  znunit  14676  psrval  14683  mplsubgfilemcl  14716  cnpnei  14946  cnntr  14952  cncnp  14957  lmtopcnp  14977  txdis1cn  15005  xmettxlem  15236  metcnp3  15238  fsumcncntop  15294  cncfco  15318  mulcncf  15335  dedekindeulemuub  15344  dedekindeulemlu  15348  dedekindicclemuub  15353  dedekindicclemlu  15357  dedekindicclemicc  15359  ivthinclemlr  15364  ivthinclemur  15366  limcimo  15392  cnplimcim  15394  plymullem1  15475  plycolemc  15485  plycj  15488  dvply2g  15493  pilem3  15510  lgsfcl2  15738  lgsval2lem  15742  lgsdir  15767  lgsne0  15770  gausslemma2dlem1a  15790  gausslemma2dlem1f1o  15792  lgsquad3  15816  umgrvad2edg  16065  usgredg2vlem2  16077  wlkvtxiedg  16199  wlkvtxiedgg  16200  clwwlkccatlem  16254  eupth2lem3lem4fi  16327  eupth2lemsfi  16332  peano4nninf  16629  nnnninfex  16645  trilpolemeq1  16665  gfsumval  16701  gfsumcl  16708