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 396   ∧ 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 397  df-3an 1088

This theorem is referenced by:  simpr1  1193  simpr1l  1229  simpr1r  1230  simpr11  1256  simpr12  1257  simpr13  1258  ispod  5513  funcnvqp  6505  dfwe2  7633  poxp  7978  cfcoflem  10037  axdc3lem  10215  fzadd2  13300  fzosubel2  13456  hashdifpr  14139  pfxccat3a  14460  sqr0lem  14961  iscatd2  17399  funcestrcsetclem9  17874  funcsetcestrclem9  17889  curf2cl  17958  yonedalem4c  18004  grpsubadd  18672  mulgnnass  18747  mulgnn0ass  18748  dprdss  19641  dprd2da  19654  srgi  19756  lsssn0  20218  zntoslem  20773  psrbaglesuppOLD  21137  blsscls  23672  iimulcl  24109  pi1grplem  24221  pi1xfrf  24225  dvconst  25090  logexprlim  26382  wwlksnextbi  28268  clwwlkccatlem  28362  clwwlkccat  28363  umgr3cyclex  28556  nvss  28964  disjdsct  31044  idlsrgmnd  31668  issgon  32100  measdivcst  32201  measdivcstALTV  32202  prv1n  33402  elmrsubrn  33491  poimirlem28  35814  ftc1anc  35867  fdc  35912  cvrnbtwn3  37297  paddasslem9  37849  paddasslem17  37857  pmapjlln1  37876  lautj  38114  lautm  38115  dfsalgen2  43887  smflimlem4  44319  lidldomnnring  45499  funcringcsetcALTV2lem9  45613  funcringcsetclem9ALTV  45636  lincresunit3lem2  45832  isthincd2  46330