Metamath Proof Explorer


Theorem nanass

Description: A characterization of when an expression involving alternative denials associates. Remark: alternative denial is commutative, see nancom . (Contributed by Richard Penner, 29-Feb-2020) (Proof shortened by Wolf Lammen, 23-Oct-2022)

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

Proof

Step Hyp Ref Expression
1 bicom1
 |-  ( ( ph <-> ch ) -> ( ch <-> ph ) )
2 nanbi2
 |-  ( ( ph <-> ch ) -> ( ( ps -/\ ph ) <-> ( ps -/\ ch ) ) )
3 1 2 nanbi12d
 |-  ( ( ph <-> ch ) -> ( ( ch -/\ ( ps -/\ ph ) ) <-> ( ph -/\ ( ps -/\ ch ) ) ) )
4 nannan
 |-  ( ( ph -/\ ( ps -/\ ch ) ) <-> ( ph -> ( ps /\ ch ) ) )
5 simpr
 |-  ( ( ps /\ ch ) -> ch )
6 5 imim2i
 |-  ( ( ph -> ( ps /\ ch ) ) -> ( ph -> ch ) )
7 4 6 sylbi
 |-  ( ( ph -/\ ( ps -/\ ch ) ) -> ( ph -> ch ) )
8 nannan
 |-  ( ( ch -/\ ( ps -/\ ph ) ) <-> ( ch -> ( ps /\ ph ) ) )
9 simpr
 |-  ( ( ps /\ ph ) -> ph )
10 9 imim2i
 |-  ( ( ch -> ( ps /\ ph ) ) -> ( ch -> ph ) )
11 8 10 sylbi
 |-  ( ( ch -/\ ( ps -/\ ph ) ) -> ( ch -> ph ) )
12 7 11 impbid21d
 |-  ( ( ch -/\ ( ps -/\ ph ) ) -> ( ( ph -/\ ( ps -/\ ch ) ) -> ( ph <-> ch ) ) )
13 nanan
 |-  ( ( ph /\ ( ps -/\ ch ) ) <-> -. ( ph -/\ ( ps -/\ ch ) ) )
14 simpl
 |-  ( ( ph /\ ( ps -/\ ch ) ) -> ph )
15 13 14 sylbir
 |-  ( -. ( ph -/\ ( ps -/\ ch ) ) -> ph )
16 nanan
 |-  ( ( ch /\ ( ps -/\ ph ) ) <-> -. ( ch -/\ ( ps -/\ ph ) ) )
17 simpl
 |-  ( ( ch /\ ( ps -/\ ph ) ) -> ch )
18 16 17 sylbir
 |-  ( -. ( ch -/\ ( ps -/\ ph ) ) -> ch )
19 pm5.1im
 |-  ( ph -> ( ch -> ( ph <-> ch ) ) )
20 15 18 19 syl2imc
 |-  ( -. ( ch -/\ ( ps -/\ ph ) ) -> ( -. ( ph -/\ ( ps -/\ ch ) ) -> ( ph <-> ch ) ) )
21 12 20 bija
 |-  ( ( ( ch -/\ ( ps -/\ ph ) ) <-> ( ph -/\ ( ps -/\ ch ) ) ) -> ( ph <-> ch ) )
22 3 21 impbii
 |-  ( ( ph <-> ch ) <-> ( ( ch -/\ ( ps -/\ ph ) ) <-> ( ph -/\ ( ps -/\ ch ) ) ) )
23 nancom
 |-  ( ( ps -/\ ph ) <-> ( ph -/\ ps ) )
24 23 nanbi2i
 |-  ( ( ch -/\ ( ps -/\ ph ) ) <-> ( ch -/\ ( ph -/\ ps ) ) )
25 nancom
 |-  ( ( ch -/\ ( ph -/\ ps ) ) <-> ( ( ph -/\ ps ) -/\ ch ) )
26 24 25 bitri
 |-  ( ( ch -/\ ( ps -/\ ph ) ) <-> ( ( ph -/\ ps ) -/\ ch ) )
27 26 bibi1i
 |-  ( ( ( ch -/\ ( ps -/\ ph ) ) <-> ( ph -/\ ( ps -/\ ch ) ) ) <-> ( ( ( ph -/\ ps ) -/\ ch ) <-> ( ph -/\ ( ps -/\ ch ) ) ) )
28 22 27 bitri
 |-  ( ( ph <-> ch ) <-> ( ( ( ph -/\ ps ) -/\ ch ) <-> ( ph -/\ ( ps -/\ ch ) ) ) )