Theorem 3ad2antr2 1190

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 716	. 2 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)
3	2	3adantr3 1172	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:  simpr2  1196  simpr2l  1233  simpr2r  1234  simpr21  1261  simpr22  1262  simpr23  1263  wereu  5650  axdc4lem  10469  ioc0  13409  funcestrcsetclem9  18160  funcsetcestrclem9  18175  grpsubadd  19011  zntoslem  21517  mdsl3  32297  dvrcan5  33231  idlsrgmnd  33529  prv1n  35453  brofs2  36095  brifs2  36096  poimirlem28  37672  ftc1anc  37725  frinfm  37759  welb  37760  fdc  37769  unichnidl  38055  cvrnbtwn2  39293  islpln2a  39567  paddss1  39836  paddss2  39837  paddasslem17  39855  tendospass  41038  funcringcsetcALTV2lem9  48273  funcringcsetclem9ALTV  48296  ldepsprlem  48448