Theorem 3ad2antr1 1189

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 717	. 2 ⊢ ((𝜑 ∧ (𝜒 ∧ 𝜓)) → 𝜃)
3	2	3adantr3 1172	1 ⊢ ((𝜑 ∧ (𝜒 ∧ 𝜓 ∧ 𝜏)) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1086

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088

This theorem is referenced by:  simpr1  1195  simpr1l  1231  simpr1r  1232  simpr11  1258  simpr12  1259  simpr13  1260  ispod  5541  funcnvqp  6556  dfwe2  7719  poxp  8070  cfcoflem  10184  axdc3lem  10362  fzadd2  13477  fzosubel2  13643  hashdifpr  14340  pfxccat3a  14663  sqrt0  15166  iscatd2  17606  funcestrcsetclem9  18073  funcsetcestrclem9  18088  curf2cl  18156  yonedalem4c  18202  grpsubadd  18960  mulgnnass  19041  mulgnn0ass  19042  dprdss  19962  dprd2da  19975  srgdilem  20129  lsssn0  20901  zntoslem  21513  sraassab  21825  blsscls  24453  iimulcl  24891  pi1grplem  25007  pi1xfrf  25011  dvconst  25876  logexprlim  27194  wwlksnextbi  29969  clwwlkccatlem  30066  clwwlkccat  30067  umgr3cyclex  30260  nvss  30670  disjdsct  32784  idlsrgmnd  33597  issgon  34282  measdivcst  34383  measdivcstALTV  34384  prv1n  35627  elmrsubrn  35716  poimirlem28  37851  ftc1anc  37904  fdc  37948  cvrnbtwn3  39558  paddasslem9  40110  paddasslem17  40118  pmapjlln1  40137  lautj  40375  lautm  40376  dfsalgen2  46606  smflimlem4  47039  lidldomnnring  48503  funcringcsetcALTV2lem9  48565  funcringcsetclem9ALTV  48588  lincresunit3lem2  48747  isthincd2  49703