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  4025  tfr1onlemaccex  6403  tfrcllemaccex  6416  phplem4on  6925  dif1enen  6938  en2eqpr  6965  unsnfidcex  6978  unsnfidcel  6979  unfidisj  6980  undifdc  6982  fiintim  6987  ssfirab  6992  suplub2ti  7062  djudom  7154  omp1eomlem  7155  difinfsnlem  7160  difinfinf  7162  ctssdclemn0  7171  ctssdc  7174  nnnninfeq2  7190  nninfisol  7194  nninfwlpoimlemginf  7237  cc3  7330  ltaddpr  7659  ltexprlemrl  7672  addcanprleml  7676  addcanprlemu  7677  aptiprleml  7701  aptiprlemu  7702  cauappcvgprlemdisj  7713  cauappcvgprlemladdrl  7719  caucvgprlemloc  7737  caucvgprlemladdrl  7740  caucvgprprlemopl  7759  caucvgprprlemloc  7765  caucvgprprlemexbt  7768  suplocexprlemrl  7779  suplocexprlemru  7781  suplocexprlemdisj  7782  suplocexprlemloc  7783  suplocexprlemub  7785  caucvgsrlemoffres  7862  suplocsrlem  7870  axcaucvglemcau  7960  axcaucvglemres  7961  negf1o  8403  apreim  8624  apsym  8627  apcotr  8628  apadd1  8629  apneg  8632  mulext1  8633  mulge0  8640  apti  8643  aprcl  8667  qapne  9707  xaddf  9913  xaddval  9914  qtri3or  10313  exbtwnzlemstep  10319  rebtwn2zlemstep  10324  addmodlteq  10472  seq3f1olemqsumk  10586  seq3f1oleml  10590  qsqeqor  10724  apexp1  10792  faclbnd  10815  hashennnuni  10853  cvg1nlemres  11132  resqrexlemoverl  11168  resqrexlemglsq  11169  resqrexlemga  11170  minmax  11376  xrmaxleim  11390  xrmaxifle  11392  xrmaxiflemab  11393  xrmaxiflemlub  11394  xrmaxiflemcom  11395  xrmaxltsup  11404  xrmaxadd  11407  xrminmax  11411  xrbdtri  11422  climrecvg1n  11494  serf0  11498  zsumdc  11530  isumss  11537  fisumss  11538  fsum3cvg3  11542  fsumcl2lem  11544  fsumadd  11552  fsummulc2  11594  divcnv  11643  cvgratz  11678  mertenslem2  11682  zproddc  11725  fprodssdc  11736  fprodmul  11737  fprodsplitdc  11742  fprodcl2lem  11751  fprodle  11786  fprodmodd  11787  p1modz1  11940  dvds2ln  11970  divalglemeunn  12065  divalglemeuneg  12067  zsupcllemstep  12085  dvdsbnd  12096  bezoutlemnewy  12136  bezoutlemstep  12137  bezoutlemmain  12138  bezoutlembi  12145  dfgcd3  12150  uzwodc  12177  nninfctlemfo  12180  lcmgcdlem  12218  cncongr1  12244  cncongr2  12245  isprm5  12283  odzdvds  12386  pclemdc  12429  pceu  12436  dvdsprmpweqle  12478  pcadd  12481  1arith  12508  4sqexercise2  12540  4sqlem13m  12544  ennnfonelemhom  12575  ennnfonelemrnh  12576  ctinfomlemom  12587  resmhm2b  13064  mhmid  13188  mhmmnd  13189  ghmgrp  13191  mulgfng  13197  conjnmzb  13353  imasabl  13409  issrg  13464  ringinvnzdiv  13549  znunit  14158  psrval  14163  cnpnei  14398  cnntr  14404  cncnp  14409  lmtopcnp  14429  txdis1cn  14457  xmettxlem  14688  metcnp3  14690  fsumcncntop  14746  cncfco  14770  mulcncf  14787  dedekindeulemuub  14796  dedekindeulemlu  14800  dedekindicclemuub  14805  dedekindicclemlu  14809  dedekindicclemicc  14811  ivthinclemlr  14816  ivthinclemur  14818  limcimo  14844  cnplimcim  14846  plymullem1  14927  plycolemc  14936  plycj  14939  pilem3  14959  lgsfcl2  15163  lgsval2lem  15167  lgsdir  15192  lgsne0  15195  gausslemma2dlem1a  15215  gausslemma2dlem1f1o  15217  lgsquad3  15241  peano4nninf  15566  trilpolemeq1  15600