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  4109  tfr1onlemaccex  6592  tfrcllemaccex  6605  phplem4on  7135  dif1enen  7150  elssdc  7175  en2eqpr  7180  unsnfidcex  7193  unsnfidcel  7194  unfidisj  7195  undifdc  7197  fiintim  7204  ssfirab  7210  suplub2ti  7305  djudom  7397  omp1eomlem  7398  difinfsnlem  7403  difinfinf  7405  ctssdclemn0  7414  ctssdc  7417  nnnninfeq2  7433  nninfisol  7437  nninfwlpoimlemginf  7480  cc3  7598  ltaddpr  7928  ltexprlemrl  7941  addcanprleml  7945  addcanprlemu  7946  aptiprleml  7970  aptiprlemu  7971  cauappcvgprlemdisj  7982  cauappcvgprlemladdrl  7988  caucvgprlemloc  8006  caucvgprlemladdrl  8009  caucvgprprlemopl  8028  caucvgprprlemloc  8034  caucvgprprlemexbt  8037  suplocexprlemrl  8048  suplocexprlemru  8050  suplocexprlemdisj  8051  suplocexprlemloc  8052  suplocexprlemub  8054  caucvgsrlemoffres  8131  suplocsrlem  8139  axcaucvglemcau  8229  axcaucvglemres  8230  negf1o  8673  apreim  8895  apsym  8898  apcotr  8899  apadd1  8900  apneg  8903  mulext1  8904  mulge0  8911  apti  8914  aprcl  8938  qapne  9992  xaddf  10199  xaddval  10200  zsupcllemstep  10614  qtri3or  10627  exbtwnzlemstep  10634  rebtwn2zlemstep  10639  addmodlteq  10787  seq3f1olemqsumk  10901  seq3f1oleml  10905  qsqeqor  11039  apexp1  11108  faclbnd  11131  hashennnuni  11170  swrdswrd  11425  swrdccatin1  11445  pfxccatin12lem3  11452  swrdccat3blem  11459  cvg1nlemres  11698  resqrexlemoverl  11734  resqrexlemglsq  11735  resqrexlemga  11736  minmax  11943  xrmaxleim  11957  xrmaxifle  11959  xrmaxiflemab  11960  xrmaxiflemlub  11961  xrmaxiflemcom  11962  xrmaxltsup  11971  xrmaxadd  11974  xrminmax  11978  xrbdtri  11989  climrecvg1n  12061  serf0  12065  zsumdc  12098  isumss  12105  fisumss  12106  fsum3cvg3  12110  fsumcl2lem  12112  fsumadd  12120  fsummulc2  12162  divcnv  12211  cvgratz  12246  mertenslem2  12250  zproddc  12293  fprodssdc  12304  fprodmul  12305  fprodsplitdc  12310  fprodcl2lem  12319  fprodle  12354  fprodmodd  12355  p1modz1  12508  dvds2ln  12538  divalglemeunn  12635  divalglemeuneg  12637  bitsfzolem  12668  dvdsbnd  12680  bezoutlemnewy  12720  bezoutlemstep  12721  bezoutlemmain  12722  bezoutlembi  12729  dfgcd3  12734  uzwodc  12761  nninfctlemfo  12764  lcmgcdlem  12802  cncongr1  12828  cncongr2  12829  isprm5  12867  odzdvds  12971  pclemdc  13014  pceu  13021  dvdsprmpweqle  13063  pcadd  13066  1arith  13093  4sqexercise2  13125  4sqlem13m  13129  ballotfilemcdc  13170  ballotfilemsle  13195  ennnfonelemhom  13253  ennnfonelemrnh  13254  ctinfomlemom  13265  resmhm2b  13747  mhmid  13871  mhmmnd  13872  ghmgrp  13874  mulgfng  13880  conjnmzb  14036  imasabl  14092  gfsumval  14105  gfsumcl  14113  prdsval  14118  issrg  14211  ringinvnzdiv  14296  znunit  14936  psrval  14943  mplsubgfilemcl  14983  cnpnei  15213  cnntr  15219  cncnp  15224  lmtopcnp  15244  txdis1cn  15272  xmettxlem  15503  metcnp3  15505  fsumcncntop  15561  cncfco  15585  mulcncf  15602  dedekindeulemuub  15611  dedekindeulemlu  15615  dedekindicclemuub  15620  dedekindicclemlu  15624  dedekindicclemicc  15626  ivthinclemlr  15631  ivthinclemur  15633  limcimo  15659  cnplimcim  15661  plymullem1  15742  plycolemc  15752  plycj  15755  dvply2g  15760  pilem3  15777  lgsfcl2  16008  lgsval2lem  16012  lgsdir  16037  lgsne0  16040  gausslemma2dlem1a  16060  gausslemma2dlem1f1o  16062  lgsquad3  16086  umgrvad2edg  16335  usgredg2vlem2  16347  wlkvtxiedg  16469  wlkvtxiedgg  16470  clwwlkccatlem  16524  eupth2lem3lem4fi  16597  eupth2lemsfi  16602  peano4nninf  16923  nnnninfex  16939  trilpolemeq1  16963  trimul0or  16984