Theorem 3ad2antr1 1205

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 729	. 2 ⊢ ((𝜑 ∧ (𝜒 ∧ 𝜓)) → 𝜃)
3	2	3adantr3 1188	1 ⊢ ((𝜑 ∧ (𝜒 ∧ 𝜓 ∧ 𝜏)) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1101

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 210  df-an 401  df-3an 1103

This theorem is referenced by:  simpr1  1211  simpr1l  1247  simpr1r  1248  simpr11  1274  simpr12  1275  simpr13  1276  ispod  5579  funcnvqp  6601  dfwe2  7773  poxp  8124  cfcoflem  10256  axdc3lem  10434  fzadd2  13587  fzosubel2  13754  hashdifpr  14452  pfxccat3a  14775  sqrt0  15292  iscatd2  17737  funcestrcsetclem9  18204  funcsetcestrclem9  18219  curf2cl  18287  yonedalem4c  18333  grpsubadd  19094  mulgnnass  19175  mulgnn0ass  19176  dprdss  20101  dprd2da  20114  srgdilem  20274  lsssn0  21047  zntoslem  21675  sraassab  21987  blsscls  24633  iimulcl  25065  pi1grplem  25177  pi1xfrf  25181  dvconst  26045  logexprlim  27355  wwlksnextbi  30184  clwwlkccatlem  30281  clwwlkccat  30282  umgr3cyclex  30475  nvss  30886  disjdsct  32989  idlsrgmnd  33749  issgon  34458  measdivcst  34559  measdivcstALTV  34560  prv1n  35856  elmrsubrn  35945  poimirlem28  38221  ftc1anc  38274  fdc  38318  cvrnbtwn3  39974  paddasslem9  40526  paddasslem17  40534  pmapjlln1  40553  lautj  40791  lautm  40792  dfsalgen2  46981  smflimlem4  47414  lidldomnnring  48924  funcringcsetcALTV2lem9  48986  funcringcsetclem9ALTV  49009  lincresunit3lem2  49179  isthincd2  50134