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  5575  funcnvqp  6605  dfwe2  7773  poxp  8132  cfcoflem  10291  axdc3lem  10469  fzadd2  13581  fzosubel2  13746  hashdifpr  14438  pfxccat3a  14761  sqrt0  15265  iscatd2  17698  funcestrcsetclem9  18165  funcsetcestrclem9  18180  curf2cl  18248  yonedalem4c  18294  grpsubadd  19016  mulgnnass  19097  mulgnn0ass  19098  dprdss  20017  dprd2da  20030  srgdilem  20157  lsssn0  20910  zntoslem  21522  sraassab  21833  blsscls  24451  iimulcl  24889  pi1grplem  25005  pi1xfrf  25009  dvconst  25875  logexprlim  27193  wwlksnextbi  29881  clwwlkccatlem  29975  clwwlkccat  29976  umgr3cyclex  30169  nvss  30579  disjdsct  32685  idlsrgmnd  33534  issgon  34159  measdivcst  34260  measdivcstALTV  34261  prv1n  35458  elmrsubrn  35547  poimirlem28  37677  ftc1anc  37730  fdc  37774  cvrnbtwn3  39299  paddasslem9  39852  paddasslem17  39860  pmapjlln1  39879  lautj  40117  lautm  40118  dfsalgen2  46337  smflimlem4  46770  lidldomnnring  48178  funcringcsetcALTV2lem9  48240  funcringcsetclem9ALTV  48263  lincresunit3lem2  48423  isthincd2  49290