Metamath Proof Explorer

Theorem an4

Description: Rearrangement of 4 conjuncts. (Contributed by NM, 10-Jul-1994)

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

Proof

Step Hyp Ref Expression
1 anass ⊢ φ ∧ ψ ∧ χ ∧ θ ↔ φ ∧ ψ ∧ χ ∧ θ
2 an12 ⊢ ψ ∧ χ ∧ θ ↔ χ ∧ ψ ∧ θ
3 2 bianass ⊢ φ ∧ ψ ∧ χ ∧ θ ↔ φ ∧ χ ∧ ψ ∧ θ
4 1 3 bitri ⊢ φ ∧ ψ ∧ χ ∧ θ ↔ φ ∧ χ ∧ ψ ∧ θ