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 ⊢φ∧ψ∧χ∧θ↔φ∧χ∧ψ∧θ