Metamath Proof Explorer

Theorem an43

Description: Rearrangement of 4 conjuncts. (Contributed by Rodolfo Medina, 24-Sep-2010) (Proof shortened by Andrew Salmon, 29-Jun-2011)

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

Proof

Step Hyp Ref Expression
1 an42 ⊢ φ ∧ θ ∧ ψ ∧ χ ↔ φ ∧ ψ ∧ χ ∧ θ
2 1 bicomi ⊢ φ ∧ ψ ∧ χ ∧ θ ↔ φ ∧ θ ∧ ψ ∧ χ