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

Syntax hints:   → wi 4   ∧ wa 396   ∧ w3a 1087

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 206  df-an 397  df-3an 1089

This theorem is referenced by:  simpr1  1194  simpr1l  1230  simpr1r  1231  simpr11  1257  simpr12  1258  simpr13  1259  ispod  5559  funcnvqp  6570  dfwe2  7713  poxp  8065  cfcoflem  10217  axdc3lem  10395  fzadd2  13486  fzosubel2  13642  hashdifpr  14325  pfxccat3a  14638  sqrt0  15138  iscatd2  17575  funcestrcsetclem9  18050  funcsetcestrclem9  18065  curf2cl  18134  yonedalem4c  18180  grpsubadd  18849  mulgnnass  18925  mulgnn0ass  18926  dprdss  19822  dprd2da  19835  srgdilem  19937  lsssn0  20465  zntoslem  21000  psrbaglesuppOLD  21364  blsscls  23900  iimulcl  24337  pi1grplem  24449  pi1xfrf  24453  dvconst  25318  logexprlim  26610  wwlksnextbi  28902  clwwlkccatlem  28996  clwwlkccat  28997  umgr3cyclex  29190  nvss  29598  disjdsct  31684  idlsrgmnd  32332  issgon  32811  measdivcst  32912  measdivcstALTV  32913  prv1n  34112  elmrsubrn  34201  poimirlem28  36179  ftc1anc  36232  fdc  36277  cvrnbtwn3  37811  paddasslem9  38364  paddasslem17  38372  pmapjlln1  38391  lautj  38629  lautm  38630  dfsalgen2  44702  smflimlem4  45135  lidldomnnring  46348  funcringcsetcALTV2lem9  46462  funcringcsetclem9ALTV  46485  lincresunit3lem2  46681  isthincd2  47178