Theorem 3ad2antr1 1188

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

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

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 1089

This theorem is referenced by:  simpr1  1194  simpr1l  1230  simpr1r  1231  simpr11  1257  simpr12  1258  simpr13  1259  ispod  5617  funcnvqp  6642  dfwe2  7809  poxp  8169  cfcoflem  10341  axdc3lem  10519  fzadd2  13619  fzosubel2  13776  hashdifpr  14464  pfxccat3a  14786  sqrt0  15290  iscatd2  17739  funcestrcsetclem9  18217  funcsetcestrclem9  18232  curf2cl  18301  yonedalem4c  18347  grpsubadd  19068  mulgnnass  19149  mulgnn0ass  19150  dprdss  20073  dprd2da  20086  srgdilem  20219  lsssn0  20969  zntoslem  21598  sraassab  21911  blsscls  24541  iimulcl  24985  pi1grplem  25101  pi1xfrf  25105  dvconst  25972  logexprlim  27287  wwlksnextbi  29927  clwwlkccatlem  30021  clwwlkccat  30022  umgr3cyclex  30215  nvss  30625  disjdsct  32714  idlsrgmnd  33507  issgon  34087  measdivcst  34188  measdivcstALTV  34189  prv1n  35399  elmrsubrn  35488  poimirlem28  37608  ftc1anc  37661  fdc  37705  cvrnbtwn3  39232  paddasslem9  39785  paddasslem17  39793  pmapjlln1  39812  lautj  40050  lautm  40051  dfsalgen2  46262  smflimlem4  46695  lidldomnnring  47959  funcringcsetcALTV2lem9  48021  funcringcsetclem9ALTV  48044  lincresunit3lem2  48209  isthincd2  48705