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  4042  tfr1onlemaccex  6441  tfrcllemaccex  6454  phplem4on  6971  dif1enen  6984  en2eqpr  7011  unsnfidcex  7024  unsnfidcel  7025  unfidisj  7026  undifdc  7028  fiintim  7035  ssfirab  7040  suplub2ti  7110  djudom  7202  omp1eomlem  7203  difinfsnlem  7208  difinfinf  7210  ctssdclemn0  7219  ctssdc  7222  nnnninfeq2  7238  nninfisol  7242  nninfwlpoimlemginf  7285  cc3  7387  ltaddpr  7717  ltexprlemrl  7730  addcanprleml  7734  addcanprlemu  7735  aptiprleml  7759  aptiprlemu  7760  cauappcvgprlemdisj  7771  cauappcvgprlemladdrl  7777  caucvgprlemloc  7795  caucvgprlemladdrl  7798  caucvgprprlemopl  7817  caucvgprprlemloc  7823  caucvgprprlemexbt  7826  suplocexprlemrl  7837  suplocexprlemru  7839  suplocexprlemdisj  7840  suplocexprlemloc  7841  suplocexprlemub  7843  caucvgsrlemoffres  7920  suplocsrlem  7928  axcaucvglemcau  8018  axcaucvglemres  8019  negf1o  8461  apreim  8683  apsym  8686  apcotr  8687  apadd1  8688  apneg  8691  mulext1  8692  mulge0  8699  apti  8702  aprcl  8726  qapne  9767  xaddf  9973  xaddval  9974  zsupcllemstep  10379  qtri3or  10390  exbtwnzlemstep  10397  rebtwn2zlemstep  10402  addmodlteq  10550  seq3f1olemqsumk  10664  seq3f1oleml  10668  qsqeqor  10802  apexp1  10870  faclbnd  10893  hashennnuni  10931  swrdswrd  11164  cvg1nlemres  11340  resqrexlemoverl  11376  resqrexlemglsq  11377  resqrexlemga  11378  minmax  11585  xrmaxleim  11599  xrmaxifle  11601  xrmaxiflemab  11602  xrmaxiflemlub  11603  xrmaxiflemcom  11604  xrmaxltsup  11613  xrmaxadd  11616  xrminmax  11620  xrbdtri  11631  climrecvg1n  11703  serf0  11707  zsumdc  11739  isumss  11746  fisumss  11747  fsum3cvg3  11751  fsumcl2lem  11753  fsumadd  11761  fsummulc2  11803  divcnv  11852  cvgratz  11887  mertenslem2  11891  zproddc  11934  fprodssdc  11945  fprodmul  11946  fprodsplitdc  11951  fprodcl2lem  11960  fprodle  11995  fprodmodd  11996  p1modz1  12149  dvds2ln  12179  divalglemeunn  12276  divalglemeuneg  12278  bitsfzolem  12309  dvdsbnd  12321  bezoutlemnewy  12361  bezoutlemstep  12362  bezoutlemmain  12363  bezoutlembi  12370  dfgcd3  12375  uzwodc  12402  nninfctlemfo  12405  lcmgcdlem  12443  cncongr1  12469  cncongr2  12470  isprm5  12508  odzdvds  12612  pclemdc  12655  pceu  12662  dvdsprmpweqle  12704  pcadd  12707  1arith  12734  4sqexercise2  12766  4sqlem13m  12770  ennnfonelemhom  12830  ennnfonelemrnh  12831  ctinfomlemom  12842  prdsval  13149  resmhm2b  13365  mhmid  13495  mhmmnd  13496  ghmgrp  13498  mulgfng  13504  conjnmzb  13660  imasabl  13716  issrg  13771  ringinvnzdiv  13856  znunit  14465  psrval  14472  mplsubgfilemcl  14505  cnpnei  14735  cnntr  14741  cncnp  14746  lmtopcnp  14766  txdis1cn  14794  xmettxlem  15025  metcnp3  15027  fsumcncntop  15083  cncfco  15107  mulcncf  15124  dedekindeulemuub  15133  dedekindeulemlu  15137  dedekindicclemuub  15142  dedekindicclemlu  15146  dedekindicclemicc  15148  ivthinclemlr  15153  ivthinclemur  15155  limcimo  15181  cnplimcim  15183  plymullem1  15264  plycolemc  15274  plycj  15277  dvply2g  15282  pilem3  15299  lgsfcl2  15527  lgsval2lem  15531  lgsdir  15556  lgsne0  15559  gausslemma2dlem1a  15579  gausslemma2dlem1f1o  15581  lgsquad3  15605  peano4nninf  16017  nnnninfex  16033  trilpolemeq1  16053