Theorem 3ad2antr1 1188

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 1171	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  1194  simpr1l  1230  simpr1r  1231  simpr11  1257  simpr12  1258  simpr13  1259  ispod  5600  funcnvqp  6629  dfwe2  7795  poxp  8154  cfcoflem  10313  axdc3lem  10491  fzadd2  13600  fzosubel2  13765  hashdifpr  14455  pfxccat3a  14777  sqrt0  15281  iscatd2  17725  funcestrcsetclem9  18194  funcsetcestrclem9  18209  curf2cl  18277  yonedalem4c  18323  grpsubadd  19047  mulgnnass  19128  mulgnn0ass  19129  dprdss  20050  dprd2da  20063  srgdilem  20190  lsssn0  20947  zntoslem  21576  sraassab  21889  blsscls  24521  iimulcl  24967  pi1grplem  25083  pi1xfrf  25087  dvconst  25953  logexprlim  27270  wwlksnextbi  29915  clwwlkccatlem  30009  clwwlkccat  30010  umgr3cyclex  30203  nvss  30613  disjdsct  32713  idlsrgmnd  33543  issgon  34125  measdivcst  34226  measdivcstALTV  34227  prv1n  35437  elmrsubrn  35526  poimirlem28  37656  ftc1anc  37709  fdc  37753  cvrnbtwn3  39278  paddasslem9  39831  paddasslem17  39839  pmapjlln1  39858  lautj  40096  lautm  40097  dfsalgen2  46361  smflimlem4  46794  lidldomnnring  48157  funcringcsetcALTV2lem9  48219  funcringcsetclem9ALTV  48242  lincresunit3lem2  48402  isthincd2  49111