Theorem ad3antrrr 489

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 274	. 2 ⊢ ((𝜑 ∧ 𝜒) → 𝜓)
3	2	ad2antrr 485	1 ⊢ ((((𝜑 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 103

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem is referenced by:  ad4antr  491  ad5ant12  515  disjiun  3982  tfr1onlemaccex  6324  tfrcllemaccex  6337  phplem4on  6841  dif1enen  6854  en2eqpr  6881  unsnfidcex  6893  unsnfidcel  6894  unfidisj  6895  undifdc  6897  fiintim  6902  ssfirab  6907  suplub2ti  6974  djudom  7066  omp1eomlem  7067  difinfsnlem  7072  difinfinf  7074  ctssdclemn0  7083  ctssdc  7086  nnnninfeq2  7101  nninfisol  7105  cc3  7217  ltaddpr  7546  ltexprlemrl  7559  addcanprleml  7563  addcanprlemu  7564  aptiprleml  7588  aptiprlemu  7589  cauappcvgprlemdisj  7600  cauappcvgprlemladdrl  7606  caucvgprlemloc  7624  caucvgprlemladdrl  7627  caucvgprprlemopl  7646  caucvgprprlemloc  7652  caucvgprprlemexbt  7655  suplocexprlemrl  7666  suplocexprlemru  7668  suplocexprlemdisj  7669  suplocexprlemloc  7670  suplocexprlemub  7672  caucvgsrlemoffres  7749  suplocsrlem  7757  axcaucvglemcau  7847  axcaucvglemres  7848  negf1o  8288  apreim  8509  apsym  8512  apcotr  8513  apadd1  8514  apneg  8517  mulext1  8518  mulge0  8525  apti  8528  aprcl  8552  qapne  9585  xaddf  9788  xaddval  9789  qtri3or  10186  exbtwnzlemstep  10191  rebtwn2zlemstep  10196  addmodlteq  10341  seq3f1olemqsumk  10442  seq3f1oleml  10446  qsqeqor  10573  apexp1  10639  faclbnd  10662  hashennnuni  10700  cvg1nlemres  10936  resqrexlemoverl  10972  resqrexlemglsq  10973  resqrexlemga  10974  minmax  11180  xrmaxleim  11194  xrmaxifle  11196  xrmaxiflemab  11197  xrmaxiflemlub  11198  xrmaxiflemcom  11199  xrmaxltsup  11208  xrmaxadd  11211  xrminmax  11215  xrbdtri  11226  climrecvg1n  11298  serf0  11302  zsumdc  11334  isumss  11341  fisumss  11342  fsum3cvg3  11346  fsumcl2lem  11348  fsumadd  11356  fsummulc2  11398  divcnv  11447  cvgratz  11482  mertenslem2  11486  zproddc  11529  fprodssdc  11540  fprodmul  11541  fprodsplitdc  11546  fprodcl2lem  11555  fprodle  11590  fprodmodd  11591  p1modz1  11743  dvds2ln  11773  divalglemeunn  11867  divalglemeuneg  11869  zsupcllemstep  11887  dvdsbnd  11898  bezoutlemnewy  11938  bezoutlemstep  11939  bezoutlemmain  11940  bezoutlembi  11947  dfgcd3  11952  uzwodc  11979  lcmgcdlem  12018  cncongr1  12044  cncongr2  12045  isprm5  12083  odzdvds  12186  pclemdc  12229  pceu  12236  dvdsprmpweqle  12277  pcadd  12280  1arith  12306  ennnfonelemhom  12357  ennnfonelemrnh  12358  ctinfomlemom  12369  cnpnei  12934  cnntr  12940  cncnp  12945  lmtopcnp  12965  txdis1cn  12993  xmettxlem  13224  metcnp3  13226  fsumcncntop  13271  cncfco  13293  mulcncf  13306  dedekindeulemuub  13310  dedekindeulemlu  13314  dedekindicclemuub  13319  dedekindicclemlu  13323  dedekindicclemicc  13325  ivthinclemlr  13330  ivthinclemur  13332  limcimo  13349  cnplimcim  13351  pilem3  13419  lgsfcl2  13622  lgsval2lem  13626  lgsdir  13651  lgsne0  13654  peano4nninf  13961  trilpolemeq1  13994