Metamath Proof Explorer

Theorem an4com24

Description: Rearrangement of 4 conjuncts: second and forth positions interchanged. (Contributed by AV, 18-Feb-2022)

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

Proof

Step Hyp Ref Expression
1 an43 ⊢ φ ∧ ψ ∧ χ ∧ θ ↔ φ ∧ θ ∧ ψ ∧ χ
2 ancom ⊢ ψ ∧ χ ↔ χ ∧ ψ
3 2 anbi2i ⊢ φ ∧ θ ∧ ψ ∧ χ ↔ φ ∧ θ ∧ χ ∧ ψ
4 1 3 bitri ⊢ φ ∧ ψ ∧ χ ∧ θ ↔ φ ∧ θ ∧ χ ∧ ψ