Metamath Proof Explorer


Theorem iscnrm3lem3

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

Ref Expression
Assertion iscnrm3lem3
|- ( ( ( ph /\ ps ) /\ ( ch /\ th ) ) <-> ( ( ph /\ ch /\ th ) /\ ps ) )

Proof

Step Hyp Ref Expression
1 anass
 |-  ( ( ( ph /\ ps ) /\ ( ch /\ th ) ) <-> ( ph /\ ( ps /\ ( ch /\ th ) ) ) )
2 anass
 |-  ( ( ( ph /\ ( ch /\ th ) ) /\ ps ) <-> ( ph /\ ( ( ch /\ th ) /\ ps ) ) )
3 3anass
 |-  ( ( ph /\ ch /\ th ) <-> ( ph /\ ( ch /\ th ) ) )
4 3 anbi1i
 |-  ( ( ( ph /\ ch /\ th ) /\ ps ) <-> ( ( ph /\ ( ch /\ th ) ) /\ ps ) )
5 ancom
 |-  ( ( ps /\ ( ch /\ th ) ) <-> ( ( ch /\ th ) /\ ps ) )
6 5 anbi2i
 |-  ( ( ph /\ ( ps /\ ( ch /\ th ) ) ) <-> ( ph /\ ( ( ch /\ th ) /\ ps ) ) )
7 2 4 6 3bitr4ri
 |-  ( ( ph /\ ( ps /\ ( ch /\ th ) ) ) <-> ( ( ph /\ ch /\ th ) /\ ps ) )
8 1 7 bitri
 |-  ( ( ( ph /\ ps ) /\ ( ch /\ th ) ) <-> ( ( ph /\ ch /\ th ) /\ ps ) )