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  4057  tfr1onlemaccex  6464  tfrcllemaccex  6477  phplem4on  6997  dif1enen  7010  en2eqpr  7037  unsnfidcex  7050  unsnfidcel  7051  unfidisj  7052  undifdc  7054  fiintim  7061  ssfirab  7066  suplub2ti  7136  djudom  7228  omp1eomlem  7229  difinfsnlem  7234  difinfinf  7236  ctssdclemn0  7245  ctssdc  7248  nnnninfeq2  7264  nninfisol  7268  nninfwlpoimlemginf  7311  cc3  7422  ltaddpr  7752  ltexprlemrl  7765  addcanprleml  7769  addcanprlemu  7770  aptiprleml  7794  aptiprlemu  7795  cauappcvgprlemdisj  7806  cauappcvgprlemladdrl  7812  caucvgprlemloc  7830  caucvgprlemladdrl  7833  caucvgprprlemopl  7852  caucvgprprlemloc  7858  caucvgprprlemexbt  7861  suplocexprlemrl  7872  suplocexprlemru  7874  suplocexprlemdisj  7875  suplocexprlemloc  7876  suplocexprlemub  7878  caucvgsrlemoffres  7955  suplocsrlem  7963  axcaucvglemcau  8053  axcaucvglemres  8054  negf1o  8496  apreim  8718  apsym  8721  apcotr  8722  apadd1  8723  apneg  8726  mulext1  8727  mulge0  8734  apti  8737  aprcl  8761  qapne  9802  xaddf  10008  xaddval  10009  zsupcllemstep  10416  qtri3or  10427  exbtwnzlemstep  10434  rebtwn2zlemstep  10439  addmodlteq  10587  seq3f1olemqsumk  10701  seq3f1oleml  10705  qsqeqor  10839  apexp1  10907  faclbnd  10930  hashennnuni  10968  swrdswrd  11203  swrdccatin1  11223  pfxccatin12lem3  11230  swrdccat3blem  11237  cvg1nlemres  11462  resqrexlemoverl  11498  resqrexlemglsq  11499  resqrexlemga  11500  minmax  11707  xrmaxleim  11721  xrmaxifle  11723  xrmaxiflemab  11724  xrmaxiflemlub  11725  xrmaxiflemcom  11726  xrmaxltsup  11735  xrmaxadd  11738  xrminmax  11742  xrbdtri  11753  climrecvg1n  11825  serf0  11829  zsumdc  11861  isumss  11868  fisumss  11869  fsum3cvg3  11873  fsumcl2lem  11875  fsumadd  11883  fsummulc2  11925  divcnv  11974  cvgratz  12009  mertenslem2  12013  zproddc  12056  fprodssdc  12067  fprodmul  12068  fprodsplitdc  12073  fprodcl2lem  12082  fprodle  12117  fprodmodd  12118  p1modz1  12271  dvds2ln  12301  divalglemeunn  12398  divalglemeuneg  12400  bitsfzolem  12431  dvdsbnd  12443  bezoutlemnewy  12483  bezoutlemstep  12484  bezoutlemmain  12485  bezoutlembi  12492  dfgcd3  12497  uzwodc  12524  nninfctlemfo  12527  lcmgcdlem  12565  cncongr1  12591  cncongr2  12592  isprm5  12630  odzdvds  12734  pclemdc  12777  pceu  12784  dvdsprmpweqle  12826  pcadd  12829  1arith  12856  4sqexercise2  12888  4sqlem13m  12892  ennnfonelemhom  12952  ennnfonelemrnh  12953  ctinfomlemom  12964  prdsval  13272  resmhm2b  13488  mhmid  13618  mhmmnd  13619  ghmgrp  13621  mulgfng  13627  conjnmzb  13783  imasabl  13839  issrg  13894  ringinvnzdiv  13979  znunit  14588  psrval  14595  mplsubgfilemcl  14628  cnpnei  14858  cnntr  14864  cncnp  14869  lmtopcnp  14889  txdis1cn  14917  xmettxlem  15148  metcnp3  15150  fsumcncntop  15206  cncfco  15230  mulcncf  15247  dedekindeulemuub  15256  dedekindeulemlu  15260  dedekindicclemuub  15265  dedekindicclemlu  15269  dedekindicclemicc  15271  ivthinclemlr  15276  ivthinclemur  15278  limcimo  15304  cnplimcim  15306  plymullem1  15387  plycolemc  15397  plycj  15400  dvply2g  15405  pilem3  15422  lgsfcl2  15650  lgsval2lem  15654  lgsdir  15679  lgsne0  15682  gausslemma2dlem1a  15702  gausslemma2dlem1f1o  15704  lgsquad3  15728  umgrvad2edg  15974  usgredg2vlem2  15986  peano4nninf  16283  nnnninfex  16299  trilpolemeq1  16319