Theorem 3ad2antr2 1189

Description: Deduction adding conjuncts to antecedent. (Contributed by NM, 27-Dec-2007.)

Hypothesis

Ref	Expression
3ad2antl.1	⊢ ((𝜑 ∧ 𝜒) → 𝜃)

Assertion

Ref	Expression
3ad2antr2	⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜏)) → 𝜃)

Proof of Theorem 3ad2antr2

Step	Hyp	Ref	Expression
1		3ad2antl.1	. . 3 ⊢ ((𝜑 ∧ 𝜒) → 𝜃)
2	1	adantrl 715	. 2 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)
3	2	3adantr3 1171	1 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒 ∧ 𝜏)) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 395   ∧ 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 207  df-an 396  df-3an 1089

This theorem is referenced by:  simpr2  1195  simpr2l  1232  simpr2r  1233  simpr21  1260  simpr22  1261  simpr23  1262  wereu  5696  axdc4lem  10524  ioc0  13454  funcestrcsetclem9  18217  funcsetcestrclem9  18232  grpsubadd  19068  zntoslem  21598  mdsl3  32348  dvrcan5  33216  idlsrgmnd  33507  prv1n  35399  brofs2  36041  brifs2  36042  poimirlem28  37608  ftc1anc  37661  frinfm  37695  welb  37696  fdc  37705  unichnidl  37991  cvrnbtwn2  39231  islpln2a  39505  paddss1  39774  paddss2  39775  paddasslem17  39793  tendospass  40976  funcringcsetcALTV2lem9  48021  funcringcsetclem9ALTV  48044  ldepsprlem  48201