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  5542  funcnvqp  6557  dfwe2  7722  poxp  8072  cfcoflem  10188  axdc3lem  10366  fzadd2  13507  fzosubel2  13674  hashdifpr  14371  pfxccat3a  14694  sqrt0  15197  iscatd2  17641  funcestrcsetclem9  18108  funcsetcestrclem9  18123  curf2cl  18191  yonedalem4c  18237  grpsubadd  18998  mulgnnass  19079  mulgnn0ass  19080  dprdss  20000  dprd2da  20013  srgdilem  20167  lsssn0  20937  zntoslem  21549  sraassab  21861  blsscls  24485  iimulcl  24917  pi1grplem  25029  pi1xfrf  25033  dvconst  25897  logexprlim  27205  wwlksnextbi  29980  clwwlkccatlem  30077  clwwlkccat  30078  umgr3cyclex  30271  nvss  30682  disjdsct  32794  idlsrgmnd  33592  issgon  34286  measdivcst  34387  measdivcstALTV  34388  prv1n  35632  elmrsubrn  35721  poimirlem28  37986  ftc1anc  38039  fdc  38083  cvrnbtwn3  39739  paddasslem9  40291  paddasslem17  40299  pmapjlln1  40318  lautj  40556  lautm  40557  dfsalgen2  46790  smflimlem4  47223  lidldomnnring  48727  funcringcsetcALTV2lem9  48789  funcringcsetclem9ALTV  48812  lincresunit3lem2  48971  isthincd2  49927