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  4078  tfr1onlemaccex  6500  tfrcllemaccex  6513  phplem4on  7037  dif1enen  7050  en2eqpr  7077  unsnfidcex  7090  unsnfidcel  7091  unfidisj  7092  undifdc  7094  fiintim  7101  ssfirab  7106  suplub2ti  7176  djudom  7268  omp1eomlem  7269  difinfsnlem  7274  difinfinf  7276  ctssdclemn0  7285  ctssdc  7288  nnnninfeq2  7304  nninfisol  7308  nninfwlpoimlemginf  7351  cc3  7462  ltaddpr  7792  ltexprlemrl  7805  addcanprleml  7809  addcanprlemu  7810  aptiprleml  7834  aptiprlemu  7835  cauappcvgprlemdisj  7846  cauappcvgprlemladdrl  7852  caucvgprlemloc  7870  caucvgprlemladdrl  7873  caucvgprprlemopl  7892  caucvgprprlemloc  7898  caucvgprprlemexbt  7901  suplocexprlemrl  7912  suplocexprlemru  7914  suplocexprlemdisj  7915  suplocexprlemloc  7916  suplocexprlemub  7918  caucvgsrlemoffres  7995  suplocsrlem  8003  axcaucvglemcau  8093  axcaucvglemres  8094  negf1o  8536  apreim  8758  apsym  8761  apcotr  8762  apadd1  8763  apneg  8766  mulext1  8767  mulge0  8774  apti  8777  aprcl  8801  qapne  9842  xaddf  10048  xaddval  10049  zsupcllemstep  10457  qtri3or  10468  exbtwnzlemstep  10475  rebtwn2zlemstep  10480  addmodlteq  10628  seq3f1olemqsumk  10742  seq3f1oleml  10746  qsqeqor  10880  apexp1  10948  faclbnd  10971  hashennnuni  11009  swrdswrd  11245  swrdccatin1  11265  pfxccatin12lem3  11272  swrdccat3blem  11279  cvg1nlemres  11504  resqrexlemoverl  11540  resqrexlemglsq  11541  resqrexlemga  11542  minmax  11749  xrmaxleim  11763  xrmaxifle  11765  xrmaxiflemab  11766  xrmaxiflemlub  11767  xrmaxiflemcom  11768  xrmaxltsup  11777  xrmaxadd  11780  xrminmax  11784  xrbdtri  11795  climrecvg1n  11867  serf0  11871  zsumdc  11903  isumss  11910  fisumss  11911  fsum3cvg3  11915  fsumcl2lem  11917  fsumadd  11925  fsummulc2  11967  divcnv  12016  cvgratz  12051  mertenslem2  12055  zproddc  12098  fprodssdc  12109  fprodmul  12110  fprodsplitdc  12115  fprodcl2lem  12124  fprodle  12159  fprodmodd  12160  p1modz1  12313  dvds2ln  12343  divalglemeunn  12440  divalglemeuneg  12442  bitsfzolem  12473  dvdsbnd  12485  bezoutlemnewy  12525  bezoutlemstep  12526  bezoutlemmain  12527  bezoutlembi  12534  dfgcd3  12539  uzwodc  12566  nninfctlemfo  12569  lcmgcdlem  12607  cncongr1  12633  cncongr2  12634  isprm5  12672  odzdvds  12776  pclemdc  12819  pceu  12826  dvdsprmpweqle  12868  pcadd  12871  1arith  12898  4sqexercise2  12930  4sqlem13m  12934  ennnfonelemhom  12994  ennnfonelemrnh  12995  ctinfomlemom  13006  prdsval  13314  resmhm2b  13530  mhmid  13660  mhmmnd  13661  ghmgrp  13663  mulgfng  13669  conjnmzb  13825  imasabl  13881  issrg  13936  ringinvnzdiv  14021  znunit  14631  psrval  14638  mplsubgfilemcl  14671  cnpnei  14901  cnntr  14907  cncnp  14912  lmtopcnp  14932  txdis1cn  14960  xmettxlem  15191  metcnp3  15193  fsumcncntop  15249  cncfco  15273  mulcncf  15290  dedekindeulemuub  15299  dedekindeulemlu  15303  dedekindicclemuub  15308  dedekindicclemlu  15312  dedekindicclemicc  15314  ivthinclemlr  15319  ivthinclemur  15321  limcimo  15347  cnplimcim  15349  plymullem1  15430  plycolemc  15440  plycj  15443  dvply2g  15448  pilem3  15465  lgsfcl2  15693  lgsval2lem  15697  lgsdir  15722  lgsne0  15725  gausslemma2dlem1a  15745  gausslemma2dlem1f1o  15747  lgsquad3  15771  umgrvad2edg  16017  usgredg2vlem2  16029  wlkvtxiedg  16066  wlkvtxiedgg  16067  peano4nninf  16402  nnnninfex  16418  trilpolemeq1  16438