Metamath Proof Explorer

Theorem an32s

Description: Swap two conjuncts in antecedent. (Contributed by NM, 13-Mar-1996)

Ref Expression
Hypothesis an32s.1 ⊢ φ ∧ ψ ∧ χ → θ
Assertion an32s ⊢ φ ∧ χ ∧ ψ → θ

Proof

Step Hyp Ref Expression
1 an32s.1 ⊢ φ ∧ ψ ∧ χ → θ
2 an32 ⊢ φ ∧ χ ∧ ψ ↔ φ ∧ ψ ∧ χ
3 2 1 sylbi ⊢ φ ∧ χ ∧ ψ → θ