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

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  498  ad5ant12  522  disjiun  4123  tfr1onlemaccex  6613  tfrcllemaccex  6626  phplem4on  7163  dif1enen  7178  elssdc  7203  en2eqpr  7208  unsnfidcex  7221  unsnfidcel  7222  unfidisj  7223  undifdc  7225  fiintim  7232  ssfirab  7238  suplub2ti  7335  djudom  7427  omp1eomlem  7428  difinfsnlem  7433  difinfinf  7435  ctssdclemn0  7444  ctssdc  7447  nnnninfeq2  7463  nninfisol  7467  nninfwlpoimlemginf  7510  cc3  7628  ltaddpr  7958  ltexprlemrl  7971  addcanprleml  7975  addcanprlemu  7976  aptiprleml  8000  aptiprlemu  8001  cauappcvgprlemdisj  8012  cauappcvgprlemladdrl  8018  caucvgprlemloc  8036  caucvgprlemladdrl  8039  caucvgprprlemopl  8058  caucvgprprlemloc  8064  caucvgprprlemexbt  8067  suplocexprlemrl  8078  suplocexprlemru  8080  suplocexprlemdisj  8081  suplocexprlemloc  8082  suplocexprlemub  8084  caucvgsrlemoffres  8161  suplocsrlem  8169  axcaucvglemcau  8259  axcaucvglemres  8260  negf1o  8703  apreim  8925  apsym  8928  apcotr  8929  apadd1  8930  apneg  8933  mulext1  8934  mulge0  8941  apti  8944  aprcl  8968  qapne  10022  xaddf  10229  xaddval  10230  zsupcllemstep  10645  qtri3or  10658  exbtwnzlemstep  10665  rebtwn2zlemstep  10670  addmodlteq  10818  seq3f1olemqsumk  10932  seq3f1oleml  10936  qsqeqor  11070  apexp1  11139  faclbnd  11162  hashennnuni  11201  swrdswrd  11460  swrdccatin1  11480  pfxccatin12lem3  11487  swrdccat3blem  11494  cvg1nlemres  11734  resqrexlemoverl  11770  resqrexlemglsq  11771  resqrexlemga  11772  minmax  11979  xrmaxleim  11993  xrmaxifle  11995  xrmaxiflemab  11996  xrmaxiflemlub  11997  xrmaxiflemcom  11998  xrmaxltsup  12007  xrmaxadd  12010  xrminmax  12014  xrbdtri  12025  climrecvg1n  12097  serf0  12101  zsumdc  12134  isumss  12141  fisumss  12142  fsum3cvg3  12146  fsumcl2lem  12148  fsumadd  12156  fsummulc2  12198  divcnv  12247  cvgratz  12282  mertenslem2  12286  zproddc  12329  fprodssdc  12340  fprodmul  12341  fprodsplitdc  12346  fprodcl2lem  12355  fprodle  12390  fprodmodd  12391  p1modz1  12544  dvds2ln  12574  divalglemeunn  12671  divalglemeuneg  12673  bitsfzolem  12704  dvdsbnd  12716  bezoutlemnewy  12756  bezoutlemstep  12757  bezoutlemmain  12758  bezoutlembi  12765  dfgcd3  12770  uzwodc  12797  nninfctlemfo  12800  lcmgcdlem  12838  cncongr1  12864  cncongr2  12865  isprm5  12903  odzdvds  13007  pclemdc  13050  pceu  13057  dvdsprmpweqle  13099  pcadd  13102  1arith  13129  4sqexercise2  13161  4sqlem13m  13165  ballotfilemcdc  13206  ballotfilemsle  13231  ennnfonelemhom  13289  ennnfonelemrnh  13290  ctinfomlemom  13301  resmhm2b  13779  mhmid  13901  mhmmnd  13902  ghmgrp  13904  mulgfng  13910  conjnmzb  14066  imasabl  14123  gsumvalfi  14135  gsumclfi  14142  gsummptfidmadd  14144  gsumsubmclfi  14146  gsumconstcmn  14149  prdsval  14156  issrg  14252  ringinvnzdiv  14338  znunit  14977  psrval  15033  mplsubgfilemcl  15073  cnpnei  15303  cnntr  15309  cncnp  15314  lmtopcnp  15334  txdis1cn  15362  xmettxlem  15593  metcnp3  15595  fsumcncntop  15651  cncfco  15675  mulcncf  15692  dedekindeulemuub  15701  dedekindeulemlu  15705  dedekindicclemuub  15710  dedekindicclemlu  15714  dedekindicclemicc  15716  ivthinclemlr  15721  ivthinclemur  15723  limcimo  15749  cnplimcim  15751  plymullem1  15832  plycolemc  15842  plycj  15845  dvply2g  15850  pilem3  15867  lgsfcl2  16108  lgsval2lem  16112  lgsdir  16137  lgsne0  16140  gausslemma2dlem1a  16160  gausslemma2dlem1f1o  16162  lgsquad3  16186  umgrvad2edg  16435  usgredg2vlem2  16447  wlkvtxiedg  16569  wlkvtxiedgg  16570  clwwlkccatlem  16624  eupth2lem3lem4fi  16697  eupth2lemsfi  16702  peano4nninf  17023  nnnninfex  17039  trilpolemeq1  17063