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