Metamath Proof Explorer


Theorem 3anassrs

Description: Associative law for conjunction applied to antecedent (eliminates syllogism). (Contributed by Mario Carneiro, 4-Jan-2017)

Ref Expression
Hypothesis 3anassrs.1 φ ψ χ θ τ
Assertion 3anassrs φ ψ χ θ τ

Proof

Step Hyp Ref Expression
1 3anassrs.1 φ ψ χ θ τ
2 1 3exp2 φ ψ χ θ τ
3 2 imp41 φ ψ χ θ τ