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  7351  ltaddpr  7681  ltexprlemrl  7694  addcanprleml  7698  addcanprlemu  7699  aptiprleml  7723  aptiprlemu  7724  cauappcvgprlemdisj  7735  cauappcvgprlemladdrl  7741  caucvgprlemloc  7759  caucvgprlemladdrl  7762  caucvgprprlemopl  7781  caucvgprprlemloc  7787  caucvgprprlemexbt  7790  suplocexprlemrl  7801  suplocexprlemru  7803  suplocexprlemdisj  7804  suplocexprlemloc  7805  suplocexprlemub  7807  caucvgsrlemoffres  7884  suplocsrlem  7892  axcaucvglemcau  7982  axcaucvglemres  7983  negf1o  8425  apreim  8647  apsym  8650  apcotr  8651  apadd1  8652  apneg  8655  mulext1  8656  mulge0  8663  apti  8666  aprcl  8690  qapne  9730  xaddf  9936  xaddval  9937  zsupcllemstep  10336  qtri3or  10347  exbtwnzlemstep  10354  rebtwn2zlemstep  10359  addmodlteq  10507  seq3f1olemqsumk  10621  seq3f1oleml  10625  qsqeqor  10759  apexp1  10827  faclbnd  10850  hashennnuni  10888  cvg1nlemres  11167  resqrexlemoverl  11203  resqrexlemglsq  11204  resqrexlemga  11205  minmax  11412  xrmaxleim  11426  xrmaxifle  11428  xrmaxiflemab  11429  xrmaxiflemlub  11430  xrmaxiflemcom  11431  xrmaxltsup  11440  xrmaxadd  11443  xrminmax  11447  xrbdtri  11458  climrecvg1n  11530  serf0  11534  zsumdc  11566  isumss  11573  fisumss  11574  fsum3cvg3  11578  fsumcl2lem  11580  fsumadd  11588  fsummulc2  11630  divcnv  11679  cvgratz  11714  mertenslem2  11718  zproddc  11761  fprodssdc  11772  fprodmul  11773  fprodsplitdc  11778  fprodcl2lem  11787  fprodle  11822  fprodmodd  11823  p1modz1  11976  dvds2ln  12006  divalglemeunn  12103  divalglemeuneg  12105  bitsfzolem  12136  dvdsbnd  12148  bezoutlemnewy  12188  bezoutlemstep  12189  bezoutlemmain  12190  bezoutlembi  12197  dfgcd3  12202  uzwodc  12229  nninfctlemfo  12232  lcmgcdlem  12270  cncongr1  12296  cncongr2  12297  isprm5  12335  odzdvds  12439  pclemdc  12482  pceu  12489  dvdsprmpweqle  12531  pcadd  12534  1arith  12561  4sqexercise2  12593  4sqlem13m  12597  ennnfonelemhom  12657  ennnfonelemrnh  12658  ctinfomlemom  12669  prdsval  12975  resmhm2b  13191  mhmid  13321  mhmmnd  13322  ghmgrp  13324  mulgfng  13330  conjnmzb  13486  imasabl  13542  issrg  13597  ringinvnzdiv  13682  znunit  14291  psrval  14296  cnpnei  14539  cnntr  14545  cncnp  14550  lmtopcnp  14570  txdis1cn  14598  xmettxlem  14829  metcnp3  14831  fsumcncntop  14887  cncfco  14911  mulcncf  14928  dedekindeulemuub  14937  dedekindeulemlu  14941  dedekindicclemuub  14946  dedekindicclemlu  14950  dedekindicclemicc  14952  ivthinclemlr  14957  ivthinclemur  14959  limcimo  14985  cnplimcim  14987  plymullem1  15068  plycolemc  15078  plycj  15081  dvply2g  15086  pilem3  15103  lgsfcl2  15331  lgsval2lem  15335  lgsdir  15360  lgsne0  15363  gausslemma2dlem1a  15383  gausslemma2dlem1f1o  15385  lgsquad3  15409  peano4nninf  15737  trilpolemeq1  15771