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  5549  funcnvqp  6564  dfwe2  7729  poxp  8080  cfcoflem  10194  axdc3lem  10372  fzadd2  13487  fzosubel2  13653  hashdifpr  14350  pfxccat3a  14673  sqrt0  15176  iscatd2  17616  funcestrcsetclem9  18083  funcsetcestrclem9  18098  curf2cl  18166  yonedalem4c  18212  grpsubadd  18973  mulgnnass  19054  mulgnn0ass  19055  dprdss  19975  dprd2da  19988  srgdilem  20142  lsssn0  20914  zntoslem  21526  sraassab  21838  blsscls  24466  iimulcl  24904  pi1grplem  25020  pi1xfrf  25024  dvconst  25889  logexprlim  27207  wwlksnextbi  29983  clwwlkccatlem  30080  clwwlkccat  30081  umgr3cyclex  30274  nvss  30685  disjdsct  32797  idlsrgmnd  33611  issgon  34305  measdivcst  34406  measdivcstALTV  34407  prv1n  35651  elmrsubrn  35740  poimirlem28  37903  ftc1anc  37956  fdc  38000  cvrnbtwn3  39656  paddasslem9  40208  paddasslem17  40216  pmapjlln1  40235  lautj  40473  lautm  40474  dfsalgen2  46703  smflimlem4  47136  lidldomnnring  48600  funcringcsetcALTV2lem9  48662  funcringcsetclem9ALTV  48685  lincresunit3lem2  48844  isthincd2  49800