Metamath Proof Explorer

Theorem bnj290

Description: /\ -manipulation. (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 3anrot ⊢ ψ ∧ χ ∧ θ ↔ χ ∧ θ ∧ ψ
2 1 anbi2i ⊢ φ ∧ ψ ∧ χ ∧ θ ↔ φ ∧ χ ∧ θ ∧ ψ
3 bnj252 ⊢ φ ∧ ψ ∧ χ ∧ θ ↔ φ ∧ ψ ∧ χ ∧ θ
4 bnj252 ⊢ φ ∧ χ ∧ θ ∧ ψ ↔ φ ∧ χ ∧ θ ∧ ψ
5 2 3 4 3bitr4i ⊢ φ ∧ ψ ∧ χ ∧ θ ↔ φ ∧ χ ∧ θ ∧ ψ