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  4078  tfr1onlemaccex  6505  tfrcllemaccex  6518  phplem4on  7042  dif1enen  7055  elssdc  7080  en2eqpr  7085  unsnfidcex  7098  unsnfidcel  7099  unfidisj  7100  undifdc  7102  fiintim  7109  ssfirab  7114  suplub2ti  7184  djudom  7276  omp1eomlem  7277  difinfsnlem  7282  difinfinf  7284  ctssdclemn0  7293  ctssdc  7296  nnnninfeq2  7312  nninfisol  7316  nninfwlpoimlemginf  7359  cc3  7470  ltaddpr  7800  ltexprlemrl  7813  addcanprleml  7817  addcanprlemu  7818  aptiprleml  7842  aptiprlemu  7843  cauappcvgprlemdisj  7854  cauappcvgprlemladdrl  7860  caucvgprlemloc  7878  caucvgprlemladdrl  7881  caucvgprprlemopl  7900  caucvgprprlemloc  7906  caucvgprprlemexbt  7909  suplocexprlemrl  7920  suplocexprlemru  7922  suplocexprlemdisj  7923  suplocexprlemloc  7924  suplocexprlemub  7926  caucvgsrlemoffres  8003  suplocsrlem  8011  axcaucvglemcau  8101  axcaucvglemres  8102  negf1o  8544  apreim  8766  apsym  8769  apcotr  8770  apadd1  8771  apneg  8774  mulext1  8775  mulge0  8782  apti  8785  aprcl  8809  qapne  9851  xaddf  10057  xaddval  10058  zsupcllemstep  10466  qtri3or  10477  exbtwnzlemstep  10484  rebtwn2zlemstep  10489  addmodlteq  10637  seq3f1olemqsumk  10751  seq3f1oleml  10755  qsqeqor  10889  apexp1  10957  faclbnd  10980  hashennnuni  11018  swrdswrd  11258  swrdccatin1  11278  pfxccatin12lem3  11285  swrdccat3blem  11292  cvg1nlemres  11517  resqrexlemoverl  11553  resqrexlemglsq  11554  resqrexlemga  11555  minmax  11762  xrmaxleim  11776  xrmaxifle  11778  xrmaxiflemab  11779  xrmaxiflemlub  11780  xrmaxiflemcom  11781  xrmaxltsup  11790  xrmaxadd  11793  xrminmax  11797  xrbdtri  11808  climrecvg1n  11880  serf0  11884  zsumdc  11916  isumss  11923  fisumss  11924  fsum3cvg3  11928  fsumcl2lem  11930  fsumadd  11938  fsummulc2  11980  divcnv  12029  cvgratz  12064  mertenslem2  12068  zproddc  12111  fprodssdc  12122  fprodmul  12123  fprodsplitdc  12128  fprodcl2lem  12137  fprodle  12172  fprodmodd  12173  p1modz1  12326  dvds2ln  12356  divalglemeunn  12453  divalglemeuneg  12455  bitsfzolem  12486  dvdsbnd  12498  bezoutlemnewy  12538  bezoutlemstep  12539  bezoutlemmain  12540  bezoutlembi  12547  dfgcd3  12552  uzwodc  12579  nninfctlemfo  12582  lcmgcdlem  12620  cncongr1  12646  cncongr2  12647  isprm5  12685  odzdvds  12789  pclemdc  12832  pceu  12839  dvdsprmpweqle  12881  pcadd  12884  1arith  12911  4sqexercise2  12943  4sqlem13m  12947  ennnfonelemhom  13007  ennnfonelemrnh  13008  ctinfomlemom  13019  prdsval  13327  resmhm2b  13543  mhmid  13673  mhmmnd  13674  ghmgrp  13676  mulgfng  13682  conjnmzb  13838  imasabl  13894  issrg  13949  ringinvnzdiv  14034  znunit  14644  psrval  14651  mplsubgfilemcl  14684  cnpnei  14914  cnntr  14920  cncnp  14925  lmtopcnp  14945  txdis1cn  14973  xmettxlem  15204  metcnp3  15206  fsumcncntop  15262  cncfco  15286  mulcncf  15303  dedekindeulemuub  15312  dedekindeulemlu  15316  dedekindicclemuub  15321  dedekindicclemlu  15325  dedekindicclemicc  15327  ivthinclemlr  15332  ivthinclemur  15334  limcimo  15360  cnplimcim  15362  plymullem1  15443  plycolemc  15453  plycj  15456  dvply2g  15461  pilem3  15478  lgsfcl2  15706  lgsval2lem  15710  lgsdir  15735  lgsne0  15738  gausslemma2dlem1a  15758  gausslemma2dlem1f1o  15760  lgsquad3  15784  umgrvad2edg  16030  usgredg2vlem2  16042  wlkvtxiedg  16117  wlkvtxiedgg  16118  clwwlkccatlem  16169  peano4nninf  16486  nnnninfex  16502  trilpolemeq1  16522