Metamath Proof Explorer

Theorem an2anr

Description: Double commutation in conjunction. (Contributed by Peter Mazsa, 27-Jun-2019)

Ref Expression
Assertion an2anr ⊢ φ ∧ ψ ∧ χ ∧ θ ↔ ψ ∧ φ ∧ θ ∧ χ

Proof

Step Hyp Ref Expression
1 ancom ⊢ φ ∧ ψ ↔ ψ ∧ φ
2 ancom ⊢ χ ∧ θ ↔ θ ∧ χ
3 1 2 anbi12i ⊢ φ ∧ ψ ∧ χ ∧ θ ↔ ψ ∧ φ ∧ θ ∧ χ