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 ) ) ) )