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  5536  funcnvqp  6546  dfwe2  7710  poxp  8061  cfcoflem  10166  axdc3lem  10344  fzadd2  13462  fzosubel2  13628  hashdifpr  14322  pfxccat3a  14644  sqrt0  15148  iscatd2  17587  funcestrcsetclem9  18054  funcsetcestrclem9  18069  curf2cl  18137  yonedalem4c  18183  grpsubadd  18907  mulgnnass  18988  mulgnn0ass  18989  dprdss  19910  dprd2da  19923  srgdilem  20077  lsssn0  20851  zntoslem  21463  sraassab  21775  blsscls  24393  iimulcl  24831  pi1grplem  24947  pi1xfrf  24951  dvconst  25816  logexprlim  27134  wwlksnextbi  29839  clwwlkccatlem  29933  clwwlkccat  29934  umgr3cyclex  30127  nvss  30537  disjdsct  32646  idlsrgmnd  33452  issgon  34096  measdivcst  34197  measdivcstALTV  34198  prv1n  35414  elmrsubrn  35503  poimirlem28  37638  ftc1anc  37691  fdc  37735  cvrnbtwn3  39265  paddasslem9  39817  paddasslem17  39825  pmapjlln1  39844  lautj  40082  lautm  40083  dfsalgen2  46332  smflimlem4  46765  lidldomnnring  48230  funcringcsetcALTV2lem9  48292  funcringcsetclem9ALTV  48315  lincresunit3lem2  48475  isthincd2  49432