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  4024  tfr1onlemaccex  6401  tfrcllemaccex  6414  phplem4on  6923  dif1enen  6936  en2eqpr  6963  unsnfidcex  6976  unsnfidcel  6977  unfidisj  6978  undifdc  6980  fiintim  6985  ssfirab  6990  suplub2ti  7060  djudom  7152  omp1eomlem  7153  difinfsnlem  7158  difinfinf  7160  ctssdclemn0  7169  ctssdc  7172  nnnninfeq2  7188  nninfisol  7192  nninfwlpoimlemginf  7235  cc3  7328  ltaddpr  7657  ltexprlemrl  7670  addcanprleml  7674  addcanprlemu  7675  aptiprleml  7699  aptiprlemu  7700  cauappcvgprlemdisj  7711  cauappcvgprlemladdrl  7717  caucvgprlemloc  7735  caucvgprlemladdrl  7738  caucvgprprlemopl  7757  caucvgprprlemloc  7763  caucvgprprlemexbt  7766  suplocexprlemrl  7777  suplocexprlemru  7779  suplocexprlemdisj  7780  suplocexprlemloc  7781  suplocexprlemub  7783  caucvgsrlemoffres  7860  suplocsrlem  7868  axcaucvglemcau  7958  axcaucvglemres  7959  negf1o  8401  apreim  8622  apsym  8625  apcotr  8626  apadd1  8627  apneg  8630  mulext1  8631  mulge0  8638  apti  8641  aprcl  8665  qapne  9704  xaddf  9910  xaddval  9911  qtri3or  10310  exbtwnzlemstep  10316  rebtwn2zlemstep  10321  addmodlteq  10469  seq3f1olemqsumk  10583  seq3f1oleml  10587  qsqeqor  10721  apexp1  10789  faclbnd  10812  hashennnuni  10850  cvg1nlemres  11129  resqrexlemoverl  11165  resqrexlemglsq  11166  resqrexlemga  11167  minmax  11373  xrmaxleim  11387  xrmaxifle  11389  xrmaxiflemab  11390  xrmaxiflemlub  11391  xrmaxiflemcom  11392  xrmaxltsup  11401  xrmaxadd  11404  xrminmax  11408  xrbdtri  11419  climrecvg1n  11491  serf0  11495  zsumdc  11527  isumss  11534  fisumss  11535  fsum3cvg3  11539  fsumcl2lem  11541  fsumadd  11549  fsummulc2  11591  divcnv  11640  cvgratz  11675  mertenslem2  11679  zproddc  11722  fprodssdc  11733  fprodmul  11734  fprodsplitdc  11739  fprodcl2lem  11748  fprodle  11783  fprodmodd  11784  p1modz1  11937  dvds2ln  11967  divalglemeunn  12062  divalglemeuneg  12064  zsupcllemstep  12082  dvdsbnd  12093  bezoutlemnewy  12133  bezoutlemstep  12134  bezoutlemmain  12135  bezoutlembi  12142  dfgcd3  12147  uzwodc  12174  nninfctlemfo  12177  lcmgcdlem  12215  cncongr1  12241  cncongr2  12242  isprm5  12280  odzdvds  12383  pclemdc  12426  pceu  12433  dvdsprmpweqle  12475  pcadd  12478  1arith  12505  4sqexercise2  12537  4sqlem13m  12541  ennnfonelemhom  12572  ennnfonelemrnh  12573  ctinfomlemom  12584  resmhm2b  13061  mhmid  13185  mhmmnd  13186  ghmgrp  13188  mulgfng  13194  conjnmzb  13350  imasabl  13406  issrg  13461  ringinvnzdiv  13546  znunit  14147  psrval  14152  cnpnei  14387  cnntr  14393  cncnp  14398  lmtopcnp  14418  txdis1cn  14446  xmettxlem  14677  metcnp3  14679  fsumcncntop  14724  cncfco  14746  mulcncf  14762  dedekindeulemuub  14771  dedekindeulemlu  14775  dedekindicclemuub  14780  dedekindicclemlu  14784  dedekindicclemicc  14786  ivthinclemlr  14791  ivthinclemur  14793  limcimo  14819  cnplimcim  14821  plymullem1  14894  pilem3  14918  lgsfcl2  15122  lgsval2lem  15126  lgsdir  15151  lgsne0  15154  gausslemma2dlem1a  15174  gausslemma2dlem1f1o  15176  peano4nninf  15496  trilpolemeq1  15530