Metamath Proof Explorer

Theorem norass

Description: A characterization of when an expression involving joint denials associates. This is identical to the case when alternative denial is associative, see nanass . Remark: Like alternative denial, joint denial is also commutative, see norcom . (Contributed by RP, 29-Oct-2023) (Proof shortened by Wolf Lammen, 17-Dec-2023)

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

Proof

Step Hyp Ref Expression
1 notbi 
 |-  ( ( ( ( ph -\/ ps ) \/ ch ) <-> ( ph \/ ( ps -\/ ch ) ) ) <-> ( -. ( ( ph -\/ ps ) \/ ch ) <-> -. ( ph \/ ( ps -\/ ch ) ) ) )
2 norasslem1 
 |-  ( ( ( ps \/ ph ) -> ch ) <-> ( ( ps -\/ ph ) \/ ch ) )
3 norasslem1 
 |-  ( ( ( ps \/ ch ) -> ph ) <-> ( ( ps -\/ ch ) \/ ph ) )
4 2 3 bibi12i 
 |-  ( ( ( ( ps \/ ph ) -> ch ) <-> ( ( ps \/ ch ) -> ph ) ) <-> ( ( ( ps -\/ ph ) \/ ch ) <-> ( ( ps -\/ ch ) \/ ph ) ) )
5 bicom 
 |-  ( ( ph <-> ch ) <-> ( ch <-> ph ) )
6 norasslem2 
 |-  ( ps -> ( ch <-> ( ( ps \/ ph ) -> ch ) ) )
7 norasslem2 
 |-  ( ps -> ( ph <-> ( ( ps \/ ch ) -> ph ) ) )
8 6 7 bibi12d 
 |-  ( ps -> ( ( ch <-> ph ) <-> ( ( ( ps \/ ph ) -> ch ) <-> ( ( ps \/ ch ) -> ph ) ) ) )
9 5 8 bitrid 
 |-  ( ps -> ( ( ph <-> ch ) <-> ( ( ( ps \/ ph ) -> ch ) <-> ( ( ps \/ ch ) -> ph ) ) ) )
10 impimprbi 
 |-  ( ( ph <-> ch ) <-> ( ( ph -> ch ) <-> ( ch -> ph ) ) )
11 norasslem3 
 |-  ( -. ps -> ( ( ph -> ch ) <-> ( ( ps \/ ph ) -> ch ) ) )
12 norasslem3 
 |-  ( -. ps -> ( ( ch -> ph ) <-> ( ( ps \/ ch ) -> ph ) ) )
13 11 12 bibi12d 
 |-  ( -. ps -> ( ( ( ph -> ch ) <-> ( ch -> ph ) ) <-> ( ( ( ps \/ ph ) -> ch ) <-> ( ( ps \/ ch ) -> ph ) ) ) )
14 10 13 bitrid 
 |-  ( -. ps -> ( ( ph <-> ch ) <-> ( ( ( ps \/ ph ) -> ch ) <-> ( ( ps \/ ch ) -> ph ) ) ) )
15 9 14 pm2.61i 
 |-  ( ( ph <-> ch ) <-> ( ( ( ps \/ ph ) -> ch ) <-> ( ( ps \/ ch ) -> ph ) ) )
16 norcom 
 |-  ( ( ph -\/ ps ) <-> ( ps -\/ ph ) )
17 16 orbi1i 
 |-  ( ( ( ph -\/ ps ) \/ ch ) <-> ( ( ps -\/ ph ) \/ ch ) )
18 orcom 
 |-  ( ( ph \/ ( ps -\/ ch ) ) <-> ( ( ps -\/ ch ) \/ ph ) )
19 17 18 bibi12i 
 |-  ( ( ( ( ph -\/ ps ) \/ ch ) <-> ( ph \/ ( ps -\/ ch ) ) ) <-> ( ( ( ps -\/ ph ) \/ ch ) <-> ( ( ps -\/ ch ) \/ ph ) ) )
20 4 15 19 3bitr4i 
 |-  ( ( ph <-> ch ) <-> ( ( ( ph -\/ ps ) \/ ch ) <-> ( ph \/ ( ps -\/ ch ) ) ) )
21 df-nor 
 |-  ( ( ( ph -\/ ps ) -\/ ch ) <-> -. ( ( ph -\/ ps ) \/ ch ) )
22 df-nor 
 |-  ( ( ph -\/ ( ps -\/ ch ) ) <-> -. ( ph \/ ( ps -\/ ch ) ) )
23 21 22 bibi12i 
 |-  ( ( ( ( ph -\/ ps ) -\/ ch ) <-> ( ph -\/ ( ps -\/ ch ) ) ) <-> ( -. ( ( ph -\/ ps ) \/ ch ) <-> -. ( ph \/ ( ps -\/ ch ) ) ) )
24 1 20 23 3bitr4i 
 |-  ( ( ph <-> ch ) <-> ( ( ( ph -\/ ps ) -\/ ch ) <-> ( ph -\/ ( ps -\/ ch ) ) ) )