Metamath Proof Explorer

Theorem an42

Description: Rearrangement of 4 conjuncts. (Contributed by NM, 7-Feb-1996)

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

Proof

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