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  6623  tfrcllemaccex  6636  phplem4on  7174  dif1enen  7189  elssdc  7214  en2eqpr  7219  unsnfidcex  7232  unsnfidcel  7233  unfidisj  7234  undifdc  7236  fiintim  7243  ssfirab  7249  suplub2ti  7348  djudom  7440  omp1eomlem  7441  difinfsnlem  7446  difinfinf  7448  ctssdclemn0  7457  ctssdc  7460  nnnninfeq2  7476  nninfisol  7480  nninfwlpoimlemginf  7523  cc3  7641  ltaddpr  7971  ltexprlemrl  7984  addcanprleml  7988  addcanprlemu  7989  aptiprleml  8013  aptiprlemu  8014  cauappcvgprlemdisj  8025  cauappcvgprlemladdrl  8031  caucvgprlemloc  8049  caucvgprlemladdrl  8052  caucvgprprlemopl  8071  caucvgprprlemloc  8077  caucvgprprlemexbt  8080  suplocexprlemrl  8091  suplocexprlemru  8093  suplocexprlemdisj  8094  suplocexprlemloc  8095  suplocexprlemub  8097  caucvgsrlemoffres  8174  suplocsrlem  8182  axcaucvglemcau  8272  axcaucvglemres  8273  negf1o  8717  apreim  8940  apsym  8943  apcotr  8944  apadd1  8945  apneg  8948  mulext1  8949  mulge0  8956  apti  8959  aprcl  8983  qapne  10056  xaddf  10264  xaddval  10265  zsupcllemstep  10680  qtri3or  10693  exbtwnzlemstep  10700  rebtwn2zlemstep  10705  addmodlteq  10857  seq3f1olemqsumk  10971  seq3f1oleml  10975  qsqeqor  11109  apexp1  11179  faclbnd  11202  hashennnuni  11241  swrdswrd  11500  swrdccatin1  11520  pfxccatin12lem3  11527  swrdccat3blem  11534  cvg1nlemres  11774  resqrexlemoverl  11810  resqrexlemglsq  11811  resqrexlemga  11812  fiidxsupcl  12019  minmax  12021  xrmaxleim  12036  xrmaxifle  12038  xrmaxiflemab  12039  xrmaxiflemlub  12040  xrmaxiflemcom  12041  xrmaxltsup  12050  xrmaxadd  12053  xrminmax  12057  xrbdtri  12068  climrecvg1n  12140  serf0  12144  zsumdc  12177  isumss  12184  fisumss  12185  fsum3cvg3  12189  fsumcl2lem  12191  fsumadd  12199  fsummulc2  12241  divcnv  12290  cvgratz  12325  mertenslem2  12329  zproddc  12372  fprodssdc  12383  fprodmul  12384  fprodsplitdc  12389  fprodcl2lem  12398  fprodle  12433  fprodmodd  12434  p1modz1  12587  dvds2ln  12617  divalglemeunn  12714  divalglemeuneg  12716  bitsfzolem  12747  dvdsbnd  12759  bezoutlemnewy  12799  bezoutlemstep  12800  bezoutlemmain  12801  bezoutlembi  12808  dfgcd3  12813  uzwodc  12840  nninfctlemfo  12843  lcmgcdlem  12881  cncongr1  12907  cncongr2  12908  isprm5  12947  sqrtrirr  13015  odzdvds  13054  pclemdc  13097  pceu  13104  dvdsprmpweqle  13146  pcadd  13149  1arith  13176  4sqexercise2  13208  4sqlem13m  13212  ballotfilemcdc  13282  ballotfilemsle  13307  ennnfonelemhom  13365  ennnfonelemrnh  13366  ctinfomlemom  13377  resmhm2b  13856  mhmid  13978  mhmmnd  13979  ghmgrp  13981  mulgfng  13987  conjnmzb  14143  imasabl  14231  gsumvalfi  14243  gsumclfi  14250  gsummptfidmadd  14252  gsumsubmclfi  14254  gsummptfidmsplit  14255  gsumconstcmn  14267  prdsval  14281  issrg  14377  ringinvnzdiv  14463  znunit  15104  psrval  15162  psrbaglefifi  15177  psrass1fi  15206  psrdifi  15207  psrdirfi  15208  mplsubgfilemcl  15227  cnpnei  15457  cnntr  15463  cncnp  15468  lmtopcnp  15488  txdis1cn  15516  xmettxlem  15747  metcnp3  15749  fsumcncntop  15805  cncfco  15829  mulcncf  15846  dedekindeulemuub  15855  dedekindeulemlu  15859  dedekindicclemuub  15864  dedekindicclemlu  15868  dedekindicclemicc  15870  ivthinclemlr  15875  ivthinclemur  15877  limcimo  15903  cnplimcim  15905  plymullem1  15986  plycolemc  15996  plycj  15999  dvply2g  16004  pilem3  16022  lgsfcl2  16342  lgsval2lem  16346  lgsdir  16371  lgsne0  16374  gausslemma2dlem1a  16394  gausslemma2dlem1f1o  16396  lgsquad3  16420  umgrvad2edg  16669  usgredg2vlem2  16681  wlkvtxiedg  16803  wlkvtxiedgg  16804  clwwlkccatlem  16858  eupth2lem3lem4fi  16931  eupth2lemsfi  16936  peano4nninf  17267  nnnninfex  17283  trilpolemeq1  17308