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  5539  funcnvqp  6554  dfwe2  7717  poxp  8068  cfcoflem  10180  axdc3lem  10358  fzadd2  13473  fzosubel2  13639  hashdifpr  14336  pfxccat3a  14659  sqrt0  15162  iscatd2  17602  funcestrcsetclem9  18069  funcsetcestrclem9  18084  curf2cl  18152  yonedalem4c  18198  grpsubadd  18956  mulgnnass  19037  mulgnn0ass  19038  dprdss  19958  dprd2da  19971  srgdilem  20125  lsssn0  20897  zntoslem  21509  sraassab  21821  blsscls  24449  iimulcl  24887  pi1grplem  25003  pi1xfrf  25007  dvconst  25872  logexprlim  27190  wwlksnextbi  29916  clwwlkccatlem  30013  clwwlkccat  30014  umgr3cyclex  30207  nvss  30617  disjdsct  32731  idlsrgmnd  33544  issgon  34229  measdivcst  34330  measdivcstALTV  34331  prv1n  35574  elmrsubrn  35663  poimirlem28  37788  ftc1anc  37841  fdc  37885  cvrnbtwn3  39475  paddasslem9  40027  paddasslem17  40035  pmapjlln1  40054  lautj  40292  lautm  40293  dfsalgen2  46527  smflimlem4  46960  lidldomnnring  48424  funcringcsetcALTV2lem9  48486  funcringcsetclem9ALTV  48509  lincresunit3lem2  48668  isthincd2  49624