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  4029  tfr1onlemaccex  6415  tfrcllemaccex  6428  phplem4on  6937  dif1enen  6950  en2eqpr  6977  unsnfidcex  6990  unsnfidcel  6991  unfidisj  6992  undifdc  6994  fiintim  7001  ssfirab  7006  suplub2ti  7076  djudom  7168  omp1eomlem  7169  difinfsnlem  7174  difinfinf  7176  ctssdclemn0  7185  ctssdc  7188  nnnninfeq2  7204  nninfisol  7208  nninfwlpoimlemginf  7251  cc3  7353  ltaddpr  7683  ltexprlemrl  7696  addcanprleml  7700  addcanprlemu  7701  aptiprleml  7725  aptiprlemu  7726  cauappcvgprlemdisj  7737  cauappcvgprlemladdrl  7743  caucvgprlemloc  7761  caucvgprlemladdrl  7764  caucvgprprlemopl  7783  caucvgprprlemloc  7789  caucvgprprlemexbt  7792  suplocexprlemrl  7803  suplocexprlemru  7805  suplocexprlemdisj  7806  suplocexprlemloc  7807  suplocexprlemub  7809  caucvgsrlemoffres  7886  suplocsrlem  7894  axcaucvglemcau  7984  axcaucvglemres  7985  negf1o  8427  apreim  8649  apsym  8652  apcotr  8653  apadd1  8654  apneg  8657  mulext1  8658  mulge0  8665  apti  8668  aprcl  8692  qapne  9732  xaddf  9938  xaddval  9939  zsupcllemstep  10338  qtri3or  10349  exbtwnzlemstep  10356  rebtwn2zlemstep  10361  addmodlteq  10509  seq3f1olemqsumk  10623  seq3f1oleml  10627  qsqeqor  10761  apexp1  10829  faclbnd  10852  hashennnuni  10890  cvg1nlemres  11169  resqrexlemoverl  11205  resqrexlemglsq  11206  resqrexlemga  11207  minmax  11414  xrmaxleim  11428  xrmaxifle  11430  xrmaxiflemab  11431  xrmaxiflemlub  11432  xrmaxiflemcom  11433  xrmaxltsup  11442  xrmaxadd  11445  xrminmax  11449  xrbdtri  11460  climrecvg1n  11532  serf0  11536  zsumdc  11568  isumss  11575  fisumss  11576  fsum3cvg3  11580  fsumcl2lem  11582  fsumadd  11590  fsummulc2  11632  divcnv  11681  cvgratz  11716  mertenslem2  11720  zproddc  11763  fprodssdc  11774  fprodmul  11775  fprodsplitdc  11780  fprodcl2lem  11789  fprodle  11824  fprodmodd  11825  p1modz1  11978  dvds2ln  12008  divalglemeunn  12105  divalglemeuneg  12107  bitsfzolem  12138  dvdsbnd  12150  bezoutlemnewy  12190  bezoutlemstep  12191  bezoutlemmain  12192  bezoutlembi  12199  dfgcd3  12204  uzwodc  12231  nninfctlemfo  12234  lcmgcdlem  12272  cncongr1  12298  cncongr2  12299  isprm5  12337  odzdvds  12441  pclemdc  12484  pceu  12491  dvdsprmpweqle  12533  pcadd  12536  1arith  12563  4sqexercise2  12595  4sqlem13m  12599  ennnfonelemhom  12659  ennnfonelemrnh  12660  ctinfomlemom  12671  prdsval  12977  resmhm2b  13193  mhmid  13323  mhmmnd  13324  ghmgrp  13326  mulgfng  13332  conjnmzb  13488  imasabl  13544  issrg  13599  ringinvnzdiv  13684  znunit  14293  psrval  14298  cnpnei  14541  cnntr  14547  cncnp  14552  lmtopcnp  14572  txdis1cn  14600  xmettxlem  14831  metcnp3  14833  fsumcncntop  14889  cncfco  14913  mulcncf  14930  dedekindeulemuub  14939  dedekindeulemlu  14943  dedekindicclemuub  14948  dedekindicclemlu  14952  dedekindicclemicc  14954  ivthinclemlr  14959  ivthinclemur  14961  limcimo  14987  cnplimcim  14989  plymullem1  15070  plycolemc  15080  plycj  15083  dvply2g  15088  pilem3  15105  lgsfcl2  15333  lgsval2lem  15337  lgsdir  15362  lgsne0  15365  gausslemma2dlem1a  15385  gausslemma2dlem1f1o  15387  lgsquad3  15411  peano4nninf  15739  nnnninfex  15755  trilpolemeq1  15775