Theorem ad3antrrr 496

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 492	1 ⊢ ((((𝜑 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) → 𝜓)

This proof depends on syntax axioms:   → wi 4   ∧ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem is used by:  ad4antr  498  ad5ant12  522  disjiun  4125  tfr1onlemaccex  6619  tfrcllemaccex  6632  phplem4on  7169  dif1enen  7184  elssdc  7209  en2eqpr  7214  unsnfidcex  7227  unsnfidcel  7228  unfidisj  7229  undifdc  7231  fiintim  7238  ssfirab  7244  suplub2ti  7341  djudom  7433  omp1eomlem  7434  difinfsnlem  7439  difinfinf  7441  ctssdclemn0  7450  ctssdc  7453  nnnninfeq2  7469  nninfisol  7473  nninfwlpoimlemginf  7516  cc3  7634  ltaddpr  7964  ltexprlemrl  7977  addcanprleml  7981  addcanprlemu  7982  aptiprleml  8006  aptiprlemu  8007  cauappcvgprlemdisj  8018  cauappcvgprlemladdrl  8024  caucvgprlemloc  8042  caucvgprlemladdrl  8045  caucvgprprlemopl  8064  caucvgprprlemloc  8070  caucvgprprlemexbt  8073  suplocexprlemrl  8084  suplocexprlemru  8086  suplocexprlemdisj  8087  suplocexprlemloc  8088  suplocexprlemub  8090  caucvgsrlemoffres  8167  suplocsrlem  8175  axcaucvglemcau  8265  axcaucvglemres  8266  negf1o  8709  apreim  8932  apsym  8935  apcotr  8936  apadd1  8937  apneg  8940  mulext1  8941  mulge0  8948  apti  8951  aprcl  8975  qapne  10041  xaddf  10248  xaddval  10249  zsupcllemstep  10664  qtri3or  10677  exbtwnzlemstep  10684  rebtwn2zlemstep  10689  addmodlteq  10837  seq3f1olemqsumk  10951  seq3f1oleml  10955  qsqeqor  11089  apexp1  11158  faclbnd  11181  hashennnuni  11220  swrdswrd  11479  swrdccatin1  11499  pfxccatin12lem3  11506  swrdccat3blem  11513  cvg1nlemres  11753  resqrexlemoverl  11789  resqrexlemglsq  11790  resqrexlemga  11791  minmax  11998  xrmaxleim  12012  xrmaxifle  12014  xrmaxiflemab  12015  xrmaxiflemlub  12016  xrmaxiflemcom  12017  xrmaxltsup  12026  xrmaxadd  12029  xrminmax  12033  xrbdtri  12044  climrecvg1n  12116  serf0  12120  zsumdc  12153  isumss  12160  fisumss  12161  fsum3cvg3  12165  fsumcl2lem  12167  fsumadd  12175  fsummulc2  12217  divcnv  12266  cvgratz  12301  mertenslem2  12305  zproddc  12348  fprodssdc  12359  fprodmul  12360  fprodsplitdc  12365  fprodcl2lem  12374  fprodle  12409  fprodmodd  12410  p1modz1  12563  dvds2ln  12593  divalglemeunn  12690  divalglemeuneg  12692  bitsfzolem  12723  dvdsbnd  12735  bezoutlemnewy  12775  bezoutlemstep  12776  bezoutlemmain  12777  bezoutlembi  12784  dfgcd3  12789  uzwodc  12816  nninfctlemfo  12819  lcmgcdlem  12857  cncongr1  12883  cncongr2  12884  isprm5  12922  odzdvds  13026  pclemdc  13069  pceu  13076  dvdsprmpweqle  13118  pcadd  13121  1arith  13148  4sqexercise2  13180  4sqlem13m  13184  ballotfilemcdc  13225  ballotfilemsle  13250  ennnfonelemhom  13308  ennnfonelemrnh  13309  ctinfomlemom  13320  resmhm2b  13798  mhmid  13920  mhmmnd  13921  ghmgrp  13923  mulgfng  13929  conjnmzb  14085  imasabl  14142  gsumvalfi  14154  gsumclfi  14161  gsummptfidmadd  14163  gsumsubmclfi  14165  gsumconstcmn  14168  prdsval  14175  issrg  14271  ringinvnzdiv  14357  znunit  14996  psrval  15052  mplsubgfilemcl  15092  cnpnei  15322  cnntr  15328  cncnp  15333  lmtopcnp  15353  txdis1cn  15381  xmettxlem  15612  metcnp3  15614  fsumcncntop  15670  cncfco  15694  mulcncf  15711  dedekindeulemuub  15720  dedekindeulemlu  15724  dedekindicclemuub  15729  dedekindicclemlu  15733  dedekindicclemicc  15735  ivthinclemlr  15740  ivthinclemur  15742  limcimo  15768  cnplimcim  15770  plymullem1  15851  plycolemc  15861  plycj  15864  dvply2g  15869  pilem3  15887  lgsfcl2  16137  lgsval2lem  16141  lgsdir  16166  lgsne0  16169  gausslemma2dlem1a  16189  gausslemma2dlem1f1o  16191  lgsquad3  16215  umgrvad2edg  16464  usgredg2vlem2  16476  wlkvtxiedg  16598  wlkvtxiedgg  16599  clwwlkccatlem  16653  eupth2lem3lem4fi  16726  eupth2lemsfi  16731  peano4nninf  17061  nnnninfex  17077  trilpolemeq1  17101