Theorem 3ad2antr1 1207

Description: Deduction adding conjuncts to antecedent. (Contributed by NM, 25-Dec-2007.)

Hypothesis

Ref	Expression
3ad2antl.1	⊢ ((𝜑 ∧ 𝜒) → 𝜃)

Assertion

Ref	Expression
3ad2antr1	⊢ ((𝜑 ∧ (𝜒 ∧ 𝜓 ∧ 𝜏)) → 𝜃)

Proof of Theorem 3ad2antr1

Step	Hyp	Ref	Expression
1		3ad2antl.1	. . 3 ⊢ ((𝜑 ∧ 𝜒) → 𝜃)
2	1	adantrr 730	. 2 ⊢ ((𝜑 ∧ (𝜒 ∧ 𝜓)) → 𝜃)
3	2	3adantr3 1190	1 ⊢ ((𝜑 ∧ (𝜒 ∧ 𝜓 ∧ 𝜏)) → 𝜃)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  simpr1  1213  simpr1l  1249  simpr1r  1250  simpr11  1276  simpr12  1277  simpr13  1278  ispod  5571  funcnvqp  6612  dfwe2  7795  poxp  8150  cfcoflem  10360  axdc3lem  10538  fzadd2  13703  fzosubel2  13870  hashdifpr  14570  pfxccat3a  14898  sqrt0  15420  iscatd2  17867  funcestrcsetclem9  18334  funcsetcestrclem9  18349  curf2cl  18417  yonedalem4c  18463  grpsubadd  19250  mulgnnass  19331  mulgnn0ass  19332  dprdss  20257  dprd2da  20270  srgdilem  20430  lsssn0  21235  zntoslem  21874  sraassab  22188  blsscls  24838  iimulcl  25270  pi1grplem  25382  pi1xfrf  25386  dvconst  26249  logexprlim  27564  wwlksnextbi  30495  clwwlkccatlem  30592  clwwlkccat  30593  umgr3cyclex  30796  nvss  31207  disjdsct  33350  idlsrgmnd  34099  issgon  34808  measdivcst  34910  measdivcstALTV  34911  prv1n  36317  elmrsubrn  36406  poimirlem28  38706  ftc1anc  38759  fdc  38819  cvrnbtwn3  40473  paddasslem9  41025  paddasslem17  41033  pmapjlln1  41052  lautj  41290  lautm  41291  dfsalgen2  47490  smflimlem4  47923  lidldomnnring  49472  funcringcsetcALTV2lem9  49534  funcringcsetclem9ALTV  49557  lincresunit3lem2  49731  isthincd2  50711