Theorem 3ad2antr1 1190

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 718	. 2 ⊢ ((𝜑 ∧ (𝜒 ∧ 𝜓)) → 𝜃)
3	2	3adantr3 1173	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  1196  simpr1l  1232  simpr1r  1233  simpr11  1259  simpr12  1260  simpr13  1261  ispod  5548  funcnvqp  6562  dfwe2  7728  poxp  8078  cfcoflem  10194  axdc3lem  10372  fzadd2  13513  fzosubel2  13680  hashdifpr  14377  pfxccat3a  14700  sqrt0  15203  iscatd2  17647  funcestrcsetclem9  18114  funcsetcestrclem9  18129  curf2cl  18197  yonedalem4c  18243  grpsubadd  19004  mulgnnass  19085  mulgnn0ass  19086  dprdss  20006  dprd2da  20019  srgdilem  20173  lsssn0  20943  zntoslem  21536  sraassab  21848  blsscls  24472  iimulcl  24904  pi1grplem  25016  pi1xfrf  25020  dvconst  25884  logexprlim  27188  wwlksnextbi  29962  clwwlkccatlem  30059  clwwlkccat  30060  umgr3cyclex  30253  nvss  30664  disjdsct  32776  idlsrgmnd  33574  issgon  34267  measdivcst  34368  measdivcstALTV  34369  prv1n  35613  elmrsubrn  35702  poimirlem28  37969  ftc1anc  38022  fdc  38066  cvrnbtwn3  39722  paddasslem9  40274  paddasslem17  40282  pmapjlln1  40301  lautj  40539  lautm  40540  dfsalgen2  46769  smflimlem4  47202  lidldomnnring  48712  funcringcsetcALTV2lem9  48774  funcringcsetclem9ALTV  48797  lincresunit3lem2  48956  isthincd2  49912