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 714	. 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 206  df-an 396  df-3an 1088

This theorem is referenced by:  simpr1  1193  simpr1l  1229  simpr1r  1230  simpr11  1256  simpr12  1257  simpr13  1258  ispod  5598  funcnvqp  6613  dfwe2  7764  poxp  8117  cfcoflem  10270  axdc3lem  10448  fzadd2  13541  fzosubel2  13697  hashdifpr  14380  pfxccat3a  14693  sqrt0  15193  iscatd2  17630  funcestrcsetclem9  18105  funcsetcestrclem9  18120  curf2cl  18189  yonedalem4c  18235  grpsubadd  18948  mulgnnass  19026  mulgnn0ass  19027  dprdss  19941  dprd2da  19954  srgdilem  20087  lsssn0  20703  zntoslem  21332  sraassab  21642  psrbaglesuppOLD  21698  blsscls  24237  iimulcl  24681  pi1grplem  24797  pi1xfrf  24801  dvconst  25667  logexprlim  26961  wwlksnextbi  29412  clwwlkccatlem  29506  clwwlkccat  29507  umgr3cyclex  29700  nvss  30110  disjdsct  32188  idlsrgmnd  32899  issgon  33416  measdivcst  33517  measdivcstALTV  33518  prv1n  34717  elmrsubrn  34806  poimirlem28  36820  ftc1anc  36873  fdc  36917  cvrnbtwn3  38450  paddasslem9  39003  paddasslem17  39011  pmapjlln1  39030  lautj  39268  lautm  39269  dfsalgen2  45357  smflimlem4  45790  lidldomnnring  46918  funcringcsetcALTV2lem9  47032  funcringcsetclem9ALTV  47055  lincresunit3lem2  47250  isthincd2  47747