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  4084  tfr1onlemaccex  6519  tfrcllemaccex  6532  phplem4on  7059  dif1enen  7074  elssdc  7099  en2eqpr  7104  unsnfidcex  7117  unsnfidcel  7118  unfidisj  7119  undifdc  7121  fiintim  7128  ssfirab  7134  suplub2ti  7205  djudom  7297  omp1eomlem  7298  difinfsnlem  7303  difinfinf  7305  ctssdclemn0  7314  ctssdc  7317  nnnninfeq2  7333  nninfisol  7337  nninfwlpoimlemginf  7380  cc3  7492  ltaddpr  7822  ltexprlemrl  7835  addcanprleml  7839  addcanprlemu  7840  aptiprleml  7864  aptiprlemu  7865  cauappcvgprlemdisj  7876  cauappcvgprlemladdrl  7882  caucvgprlemloc  7900  caucvgprlemladdrl  7903  caucvgprprlemopl  7922  caucvgprprlemloc  7928  caucvgprprlemexbt  7931  suplocexprlemrl  7942  suplocexprlemru  7944  suplocexprlemdisj  7945  suplocexprlemloc  7946  suplocexprlemub  7948  caucvgsrlemoffres  8025  suplocsrlem  8033  axcaucvglemcau  8123  axcaucvglemres  8124  negf1o  8566  apreim  8788  apsym  8791  apcotr  8792  apadd1  8793  apneg  8796  mulext1  8797  mulge0  8804  apti  8807  aprcl  8831  qapne  9878  xaddf  10084  xaddval  10085  zsupcllemstep  10495  qtri3or  10506  exbtwnzlemstep  10513  rebtwn2zlemstep  10518  addmodlteq  10666  seq3f1olemqsumk  10780  seq3f1oleml  10784  qsqeqor  10918  apexp1  10986  faclbnd  11009  hashennnuni  11047  swrdswrd  11295  swrdccatin1  11315  pfxccatin12lem3  11322  swrdccat3blem  11329  cvg1nlemres  11568  resqrexlemoverl  11604  resqrexlemglsq  11605  resqrexlemga  11606  minmax  11813  xrmaxleim  11827  xrmaxifle  11829  xrmaxiflemab  11830  xrmaxiflemlub  11831  xrmaxiflemcom  11832  xrmaxltsup  11841  xrmaxadd  11844  xrminmax  11848  xrbdtri  11859  climrecvg1n  11931  serf0  11935  zsumdc  11968  isumss  11975  fisumss  11976  fsum3cvg3  11980  fsumcl2lem  11982  fsumadd  11990  fsummulc2  12032  divcnv  12081  cvgratz  12116  mertenslem2  12120  zproddc  12163  fprodssdc  12174  fprodmul  12175  fprodsplitdc  12180  fprodcl2lem  12189  fprodle  12224  fprodmodd  12225  p1modz1  12378  dvds2ln  12408  divalglemeunn  12505  divalglemeuneg  12507  bitsfzolem  12538  dvdsbnd  12550  bezoutlemnewy  12590  bezoutlemstep  12591  bezoutlemmain  12592  bezoutlembi  12599  dfgcd3  12604  uzwodc  12631  nninfctlemfo  12634  lcmgcdlem  12672  cncongr1  12698  cncongr2  12699  isprm5  12737  odzdvds  12841  pclemdc  12884  pceu  12891  dvdsprmpweqle  12933  pcadd  12936  1arith  12963  4sqexercise2  12995  4sqlem13m  12999  ennnfonelemhom  13059  ennnfonelemrnh  13060  ctinfomlemom  13071  prdsval  13379  resmhm2b  13595  mhmid  13725  mhmmnd  13726  ghmgrp  13728  mulgfng  13734  conjnmzb  13890  imasabl  13946  issrg  14002  ringinvnzdiv  14087  znunit  14697  psrval  14704  mplsubgfilemcl  14742  cnpnei  14972  cnntr  14978  cncnp  14983  lmtopcnp  15003  txdis1cn  15031  xmettxlem  15262  metcnp3  15264  fsumcncntop  15320  cncfco  15344  mulcncf  15361  dedekindeulemuub  15370  dedekindeulemlu  15374  dedekindicclemuub  15379  dedekindicclemlu  15383  dedekindicclemicc  15385  ivthinclemlr  15390  ivthinclemur  15392  limcimo  15418  cnplimcim  15420  plymullem1  15501  plycolemc  15511  plycj  15514  dvply2g  15519  pilem3  15536  lgsfcl2  15764  lgsval2lem  15768  lgsdir  15793  lgsne0  15796  gausslemma2dlem1a  15816  gausslemma2dlem1f1o  15818  lgsquad3  15842  umgrvad2edg  16091  usgredg2vlem2  16103  wlkvtxiedg  16225  wlkvtxiedgg  16226  clwwlkccatlem  16280  eupth2lem3lem4fi  16353  eupth2lemsfi  16358  peano4nninf  16671  nnnninfex  16687  trilpolemeq1  16711  gfsumval  16748  gfsumcl  16755