Metamath Proof Explorer


Theorem 3comr

Description: Commutation in antecedent. Rotate right. (Contributed by NM, 28-Jan-1996) Theorems shortened and reordered. (Revised by Wolf Lammen, 9-Apr-2022)

Ref Expression
Hypothesis 3exp.1 ⊢ φ ∧ ψ ∧ χ → θ
Assertion 3comr ⊢ χ ∧ φ ∧ ψ → θ

Proof

Step Hyp Ref Expression
1 3exp.1 ⊢ φ ∧ ψ ∧ χ → θ
2 1 3com12 ⊢ ψ ∧ φ ∧ χ → θ
3 2 3com13 ⊢ χ ∧ φ ∧ ψ → θ