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  3996  tfr1onlemaccex  6344  tfrcllemaccex  6357  phplem4on  6862  dif1enen  6875  en2eqpr  6902  unsnfidcex  6914  unsnfidcel  6915  unfidisj  6916  undifdc  6918  fiintim  6923  ssfirab  6928  suplub2ti  6995  djudom  7087  omp1eomlem  7088  difinfsnlem  7093  difinfinf  7095  ctssdclemn0  7104  ctssdc  7107  nnnninfeq2  7122  nninfisol  7126  nninfwlpoimlemginf  7169  cc3  7262  ltaddpr  7591  ltexprlemrl  7604  addcanprleml  7608  addcanprlemu  7609  aptiprleml  7633  aptiprlemu  7634  cauappcvgprlemdisj  7645  cauappcvgprlemladdrl  7651  caucvgprlemloc  7669  caucvgprlemladdrl  7672  caucvgprprlemopl  7691  caucvgprprlemloc  7697  caucvgprprlemexbt  7700  suplocexprlemrl  7711  suplocexprlemru  7713  suplocexprlemdisj  7714  suplocexprlemloc  7715  suplocexprlemub  7717  caucvgsrlemoffres  7794  suplocsrlem  7802  axcaucvglemcau  7892  axcaucvglemres  7893  negf1o  8333  apreim  8554  apsym  8557  apcotr  8558  apadd1  8559  apneg  8562  mulext1  8563  mulge0  8570  apti  8573  aprcl  8597  qapne  9633  xaddf  9838  xaddval  9839  qtri3or  10236  exbtwnzlemstep  10241  rebtwn2zlemstep  10246  addmodlteq  10391  seq3f1olemqsumk  10492  seq3f1oleml  10496  qsqeqor  10623  apexp1  10689  faclbnd  10712  hashennnuni  10750  cvg1nlemres  10985  resqrexlemoverl  11021  resqrexlemglsq  11022  resqrexlemga  11023  minmax  11229  xrmaxleim  11243  xrmaxifle  11245  xrmaxiflemab  11246  xrmaxiflemlub  11247  xrmaxiflemcom  11248  xrmaxltsup  11257  xrmaxadd  11260  xrminmax  11264  xrbdtri  11275  climrecvg1n  11347  serf0  11351  zsumdc  11383  isumss  11390  fisumss  11391  fsum3cvg3  11395  fsumcl2lem  11397  fsumadd  11405  fsummulc2  11447  divcnv  11496  cvgratz  11531  mertenslem2  11535  zproddc  11578  fprodssdc  11589  fprodmul  11590  fprodsplitdc  11595  fprodcl2lem  11604  fprodle  11639  fprodmodd  11640  p1modz1  11792  dvds2ln  11822  divalglemeunn  11916  divalglemeuneg  11918  zsupcllemstep  11936  dvdsbnd  11947  bezoutlemnewy  11987  bezoutlemstep  11988  bezoutlemmain  11989  bezoutlembi  11996  dfgcd3  12001  uzwodc  12028  lcmgcdlem  12067  cncongr1  12093  cncongr2  12094  isprm5  12132  odzdvds  12235  pclemdc  12278  pceu  12285  dvdsprmpweqle  12326  pcadd  12329  1arith  12355  ennnfonelemhom  12406  ennnfonelemrnh  12407  ctinfomlemom  12418  mhmid  12907  mhmmnd  12908  ghmgrp  12910  mulgfng  12915  issrg  13048  ringinvnzdiv  13127  cnpnei  13501  cnntr  13507  cncnp  13512  lmtopcnp  13532  txdis1cn  13560  xmettxlem  13791  metcnp3  13793  fsumcncntop  13838  cncfco  13860  mulcncf  13873  dedekindeulemuub  13877  dedekindeulemlu  13881  dedekindicclemuub  13886  dedekindicclemlu  13890  dedekindicclemicc  13892  ivthinclemlr  13897  ivthinclemur  13899  limcimo  13916  cnplimcim  13918  pilem3  13986  lgsfcl2  14189  lgsval2lem  14193  lgsdir  14218  lgsne0  14221  peano4nninf  14526  trilpolemeq1  14559