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  5548  funcnvqp  6564  dfwe2  7730  poxp  8084  cfcoflem  10201  axdc3lem  10379  fzadd2  13496  fzosubel2  13662  hashdifpr  14356  pfxccat3a  14679  sqrt0  15183  iscatd2  17622  funcestrcsetclem9  18089  funcsetcestrclem9  18104  curf2cl  18172  yonedalem4c  18218  grpsubadd  18942  mulgnnass  19023  mulgnn0ass  19024  dprdss  19945  dprd2da  19958  srgdilem  20112  lsssn0  20886  zntoslem  21498  sraassab  21810  blsscls  24428  iimulcl  24866  pi1grplem  24982  pi1xfrf  24986  dvconst  25851  logexprlim  27169  wwlksnextbi  29874  clwwlkccatlem  29968  clwwlkccat  29969  umgr3cyclex  30162  nvss  30572  disjdsct  32676  idlsrgmnd  33478  issgon  34106  measdivcst  34207  measdivcstALTV  34208  prv1n  35411  elmrsubrn  35500  poimirlem28  37635  ftc1anc  37688  fdc  37732  cvrnbtwn3  39262  paddasslem9  39815  paddasslem17  39823  pmapjlln1  39842  lautj  40080  lautm  40081  dfsalgen2  46332  smflimlem4  46765  lidldomnnring  48217  funcringcsetcALTV2lem9  48279  funcringcsetclem9ALTV  48302  lincresunit3lem2  48462  isthincd2  49419