Theorem 3ad2antr1 1187

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 1170	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  1193  simpr1l  1229  simpr1r  1230  simpr11  1256  simpr12  1257  simpr13  1258  ispod  5606  funcnvqp  6632  dfwe2  7793  poxp  8152  cfcoflem  10310  axdc3lem  10488  fzadd2  13596  fzosubel2  13761  hashdifpr  14451  pfxccat3a  14773  sqrt0  15277  iscatd2  17726  funcestrcsetclem9  18204  funcsetcestrclem9  18219  curf2cl  18288  yonedalem4c  18334  grpsubadd  19059  mulgnnass  19140  mulgnn0ass  19141  dprdss  20064  dprd2da  20077  srgdilem  20210  lsssn0  20964  zntoslem  21593  sraassab  21906  blsscls  24536  iimulcl  24980  pi1grplem  25096  pi1xfrf  25100  dvconst  25967  logexprlim  27284  wwlksnextbi  29924  clwwlkccatlem  30018  clwwlkccat  30019  umgr3cyclex  30212  nvss  30622  disjdsct  32718  idlsrgmnd  33522  issgon  34104  measdivcst  34205  measdivcstALTV  34206  prv1n  35416  elmrsubrn  35505  poimirlem28  37635  ftc1anc  37688  fdc  37732  cvrnbtwn3  39258  paddasslem9  39811  paddasslem17  39819  pmapjlln1  39838  lautj  40076  lautm  40077  dfsalgen2  46297  smflimlem4  46730  lidldomnnring  48080  funcringcsetcALTV2lem9  48142  funcringcsetclem9ALTV  48165  lincresunit3lem2  48326  isthincd2  48838