Theorem 3ad2antr1 1207

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  simpr1  1213  simpr1l  1249  simpr1r  1250  simpr11  1276  simpr12  1277  simpr13  1278  ispod  5568  funcnvqp  6604  dfwe2  7788  poxp  8140  cfcoflem  10350  axdc3lem  10528  fzadd2  13693  fzosubel2  13860  hashdifpr  14560  pfxccat3a  14887  sqrt0  15408  iscatd2  17855  funcestrcsetclem9  18322  funcsetcestrclem9  18337  curf2cl  18405  yonedalem4c  18451  grpsubadd  19238  mulgnnass  19319  mulgnn0ass  19320  dprdss  20245  dprd2da  20258  srgdilem  20418  lsssn0  21223  zntoslem  21862  sraassab  22176  blsscls  24826  iimulcl  25258  pi1grplem  25370  pi1xfrf  25374  dvconst  26237  logexprlim  27552  wwlksnextbi  30483  clwwlkccatlem  30580  clwwlkccat  30581  umgr3cyclex  30784  nvss  31195  disjdsct  33296  idlsrgmnd  34046  issgon  34755  measdivcst  34857  measdivcstALTV  34858  prv1n  36196  elmrsubrn  36285  poimirlem28  38566  ftc1anc  38619  fdc  38679  cvrnbtwn3  40333  paddasslem9  40885  paddasslem17  40893  pmapjlln1  40912  lautj  41150  lautm  41151  dfsalgen2  47350  smflimlem4  47783  lidldomnnring  49332  funcringcsetcALTV2lem9  49394  funcringcsetclem9ALTV  49417  lincresunit3lem2  49591  isthincd2  50544