Theorem 3ad2antr1 1186

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1085

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 1087

This theorem is referenced by:  simpr1  1192  simpr1l  1228  simpr1r  1229  simpr11  1255  simpr12  1256  simpr13  1257  ispod  5503  funcnvqp  6482  dfwe2  7602  poxp  7940  cfcoflem  9959  axdc3lem  10137  fzadd2  13220  fzosubel2  13375  hashdifpr  14058  pfxccat3a  14379  sqr0lem  14880  iscatd2  17307  funcestrcsetclem9  17781  funcsetcestrclem9  17796  curf2cl  17865  yonedalem4c  17911  grpsubadd  18578  mulgnnass  18653  mulgnn0ass  18654  dprdss  19547  dprd2da  19560  srgi  19662  lsssn0  20124  zntoslem  20676  psrbaglesuppOLD  21038  blsscls  23569  iimulcl  24006  pi1grplem  24118  pi1xfrf  24122  dvconst  24986  logexprlim  26278  wwlksnextbi  28160  clwwlkccatlem  28254  clwwlkccat  28255  umgr3cyclex  28448  nvss  28856  disjdsct  30937  idlsrgmnd  31561  issgon  31991  measdivcst  32092  measdivcstALTV  32093  prv1n  33293  elmrsubrn  33382  poimirlem28  35732  ftc1anc  35785  fdc  35830  cvrnbtwn3  37217  paddasslem9  37769  paddasslem17  37777  pmapjlln1  37796  lautj  38034  lautm  38035  dfsalgen2  43770  smflimlem4  44196  lidldomnnring  45376  funcringcsetcALTV2lem9  45490  funcringcsetclem9ALTV  45513  lincresunit3lem2  45709  isthincd2  46207