Theorem 3ad2antr2 1227

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

Syntax hints:   → wi 4   ∧ wa 384   ∧ w3a 1037

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 197  df-an 386  df-3an 1039

This theorem is referenced by:  wereu  5110  axdc4lem  9277  ioc0  12222  funcestrcsetclem9  16788  funcsetcestrclem9  16803  grpsubadd  17503  psrbaglesupp  19368  zntoslem  19905  trcfilu  22098  mdsl3  29175  dvrcan5  29793  brofs2  32184  brifs2  32185  poimirlem28  33437  ftc1anc  33493  frinfm  33530  welb  33531  fdc  33541  unichnidl  33830  cvrnbtwn2  34562  islpln2a  34834  paddss1  35103  paddss2  35104  paddasslem17  35122  tendospass  36308  funcringcsetcALTV2lem9  42044  funcringcsetclem9ALTV  42067  ldepsprlem  42261