Metamath Proof Explorer

Theorem iscnrm3lem3

Description: Lemma for iscnrm3lem4 . (Contributed by Zhi Wang, 4-Sep-2024)

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

Proof

Step Hyp Ref Expression
1 anass ⊢ φ ∧ ψ ∧ χ ∧ θ ↔ φ ∧ ψ ∧ χ ∧ θ
2 anass ⊢ φ ∧ χ ∧ θ ∧ ψ ↔ φ ∧ χ ∧ θ ∧ ψ
3 3anass ⊢ φ ∧ χ ∧ θ ↔ φ ∧ χ ∧ θ
4 3 anbi1i ⊢ φ ∧ χ ∧ θ ∧ ψ ↔ φ ∧ χ ∧ θ ∧ ψ
5 ancom ⊢ ψ ∧ χ ∧ θ ↔ χ ∧ θ ∧ ψ
6 5 anbi2i ⊢ φ ∧ ψ ∧ χ ∧ θ ↔ φ ∧ χ ∧ θ ∧ ψ
7 2 4 6 3bitr4ri ⊢ φ ∧ ψ ∧ χ ∧ θ ↔ φ ∧ χ ∧ θ ∧ ψ
8 1 7 bitri ⊢ φ ∧ ψ ∧ χ ∧ θ ↔ φ ∧ χ ∧ θ ∧ ψ