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  3998  tfr1onlemaccex  6348  tfrcllemaccex  6361  phplem4on  6866  dif1enen  6879  en2eqpr  6906  unsnfidcex  6918  unsnfidcel  6919  unfidisj  6920  undifdc  6922  fiintim  6927  ssfirab  6932  suplub2ti  6999  djudom  7091  omp1eomlem  7092  difinfsnlem  7097  difinfinf  7099  ctssdclemn0  7108  ctssdc  7111  nnnninfeq2  7126  nninfisol  7130  nninfwlpoimlemginf  7173  cc3  7266  ltaddpr  7595  ltexprlemrl  7608  addcanprleml  7612  addcanprlemu  7613  aptiprleml  7637  aptiprlemu  7638  cauappcvgprlemdisj  7649  cauappcvgprlemladdrl  7655  caucvgprlemloc  7673  caucvgprlemladdrl  7676  caucvgprprlemopl  7695  caucvgprprlemloc  7701  caucvgprprlemexbt  7704  suplocexprlemrl  7715  suplocexprlemru  7717  suplocexprlemdisj  7718  suplocexprlemloc  7719  suplocexprlemub  7721  caucvgsrlemoffres  7798  suplocsrlem  7806  axcaucvglemcau  7896  axcaucvglemres  7897  negf1o  8338  apreim  8559  apsym  8562  apcotr  8563  apadd1  8564  apneg  8567  mulext1  8568  mulge0  8575  apti  8578  aprcl  8602  qapne  9638  xaddf  9843  xaddval  9844  qtri3or  10242  exbtwnzlemstep  10247  rebtwn2zlemstep  10252  addmodlteq  10397  seq3f1olemqsumk  10498  seq3f1oleml  10502  qsqeqor  10630  apexp1  10697  faclbnd  10720  hashennnuni  10758  cvg1nlemres  10993  resqrexlemoverl  11029  resqrexlemglsq  11030  resqrexlemga  11031  minmax  11237  xrmaxleim  11251  xrmaxifle  11253  xrmaxiflemab  11254  xrmaxiflemlub  11255  xrmaxiflemcom  11256  xrmaxltsup  11265  xrmaxadd  11268  xrminmax  11272  xrbdtri  11283  climrecvg1n  11355  serf0  11359  zsumdc  11391  isumss  11398  fisumss  11399  fsum3cvg3  11403  fsumcl2lem  11405  fsumadd  11413  fsummulc2  11455  divcnv  11504  cvgratz  11539  mertenslem2  11543  zproddc  11586  fprodssdc  11597  fprodmul  11598  fprodsplitdc  11603  fprodcl2lem  11612  fprodle  11647  fprodmodd  11648  p1modz1  11800  dvds2ln  11830  divalglemeunn  11925  divalglemeuneg  11927  zsupcllemstep  11945  dvdsbnd  11956  bezoutlemnewy  11996  bezoutlemstep  11997  bezoutlemmain  11998  bezoutlembi  12005  dfgcd3  12010  uzwodc  12037  lcmgcdlem  12076  cncongr1  12102  cncongr2  12103  isprm5  12141  odzdvds  12244  pclemdc  12287  pceu  12294  dvdsprmpweqle  12335  pcadd  12338  1arith  12364  ennnfonelemhom  12415  ennnfonelemrnh  12416  ctinfomlemom  12427  mhmid  12978  mhmmnd  12979  ghmgrp  12981  mulgfng  12986  issrg  13146  ringinvnzdiv  13225  cnpnei  13689  cnntr  13695  cncnp  13700  lmtopcnp  13720  txdis1cn  13748  xmettxlem  13979  metcnp3  13981  fsumcncntop  14026  cncfco  14048  mulcncf  14061  dedekindeulemuub  14065  dedekindeulemlu  14069  dedekindicclemuub  14074  dedekindicclemlu  14078  dedekindicclemicc  14080  ivthinclemlr  14085  ivthinclemur  14087  limcimo  14104  cnplimcim  14106  pilem3  14174  lgsfcl2  14377  lgsval2lem  14381  lgsdir  14406  lgsne0  14409  peano4nninf  14725  trilpolemeq1  14758