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