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  5555  funcnvqp  6580  dfwe2  7750  poxp  8107  cfcoflem  10225  axdc3lem  10403  fzadd2  13520  fzosubel2  13686  hashdifpr  14380  pfxccat3a  14703  sqrt0  15207  iscatd2  17642  funcestrcsetclem9  18109  funcsetcestrclem9  18124  curf2cl  18192  yonedalem4c  18238  grpsubadd  18960  mulgnnass  19041  mulgnn0ass  19042  dprdss  19961  dprd2da  19974  srgdilem  20101  lsssn0  20854  zntoslem  21466  sraassab  21777  blsscls  24395  iimulcl  24833  pi1grplem  24949  pi1xfrf  24953  dvconst  25818  logexprlim  27136  wwlksnextbi  29824  clwwlkccatlem  29918  clwwlkccat  29919  umgr3cyclex  30112  nvss  30522  disjdsct  32626  idlsrgmnd  33485  issgon  34113  measdivcst  34214  measdivcstALTV  34215  prv1n  35418  elmrsubrn  35507  poimirlem28  37642  ftc1anc  37695  fdc  37739  cvrnbtwn3  39269  paddasslem9  39822  paddasslem17  39830  pmapjlln1  39849  lautj  40087  lautm  40088  dfsalgen2  46339  smflimlem4  46772  lidldomnnring  48221  funcringcsetcALTV2lem9  48283  funcringcsetclem9ALTV  48306  lincresunit3lem2  48466  isthincd2  49423