Metamath Proof Explorer

Theorem norassOLD

Description: Obsolete version of norass as of 17-Dec-2023. (Contributed by RP, 29-Oct-2023) (Proof modification is discouraged.) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 id 
 |-  ( ( ph <-> ch ) -> ( ph <-> ch ) )
2 1 notbid 
 |-  ( ( ph <-> ch ) -> ( -. ph <-> -. ch ) )
3 2 bicomd 
 |-  ( ( ph <-> ch ) -> ( -. ch <-> -. ph ) )
4 2 anbi2d 
 |-  ( ( ph <-> ch ) -> ( ( -. ps /\ -. ph ) <-> ( -. ps /\ -. ch ) ) )
5 4 notbid 
 |-  ( ( ph <-> ch ) -> ( -. ( -. ps /\ -. ph ) <-> -. ( -. ps /\ -. ch ) ) )
6 3 5 anbi12d 
 |-  ( ( ph <-> ch ) -> ( ( -. ch /\ -. ( -. ps /\ -. ph ) ) <-> ( -. ph /\ -. ( -. ps /\ -. ch ) ) ) )
7 olc 
 |-  ( ph -> ( ps \/ ph ) )
8 oran 
 |-  ( ( ps \/ ph ) <-> -. ( -. ps /\ -. ph ) )
9 7 8 sylib 
 |-  ( ph -> -. ( -. ps /\ -. ph ) )
10 9 anim1ci 
 |-  ( ( ph /\ -. ch ) -> ( -. ch /\ -. ( -. ps /\ -. ph ) ) )
11 animorl 
 |-  ( ( ph /\ -. ch ) -> ( ph \/ ( -. ps /\ -. ch ) ) )
12 oran 
 |-  ( ( ph \/ ( -. ps /\ -. ch ) ) <-> -. ( -. ph /\ -. ( -. ps /\ -. ch ) ) )
13 11 12 sylib 
 |-  ( ( ph /\ -. ch ) -> -. ( -. ph /\ -. ( -. ps /\ -. ch ) ) )
14 10 13 jcnd 
 |-  ( ( ph /\ -. ch ) -> -. ( ( -. ch /\ -. ( -. ps /\ -. ph ) ) -> ( -. ph /\ -. ( -. ps /\ -. ch ) ) ) )
15 14 ex 
 |-  ( ph -> ( -. ch -> -. ( ( -. ch /\ -. ( -. ps /\ -. ph ) ) -> ( -. ph /\ -. ( -. ps /\ -. ch ) ) ) ) )
16 15 con4d 
 |-  ( ph -> ( ( ( -. ch /\ -. ( -. ps /\ -. ph ) ) -> ( -. ph /\ -. ( -. ps /\ -. ch ) ) ) -> ch ) )
17 16 com12 
 |-  ( ( ( -. ch /\ -. ( -. ps /\ -. ph ) ) -> ( -. ph /\ -. ( -. ps /\ -. ch ) ) ) -> ( ph -> ch ) )
18 olc 
 |-  ( ch -> ( ps \/ ch ) )
19 oran 
 |-  ( ( ps \/ ch ) <-> -. ( -. ps /\ -. ch ) )
20 18 19 sylib 
 |-  ( ch -> -. ( -. ps /\ -. ch ) )
21 20 anim1ci 
 |-  ( ( ch /\ -. ph ) -> ( -. ph /\ -. ( -. ps /\ -. ch ) ) )
22 animorl 
 |-  ( ( ch /\ -. ph ) -> ( ch \/ ( -. ps /\ -. ph ) ) )
23 oran 
 |-  ( ( ch \/ ( -. ps /\ -. ph ) ) <-> -. ( -. ch /\ -. ( -. ps /\ -. ph ) ) )
24 22 23 sylib 
 |-  ( ( ch /\ -. ph ) -> -. ( -. ch /\ -. ( -. ps /\ -. ph ) ) )
25 21 24 jcnd 
 |-  ( ( ch /\ -. ph ) -> -. ( ( -. ph /\ -. ( -. ps /\ -. ch ) ) -> ( -. ch /\ -. ( -. ps /\ -. ph ) ) ) )
26 25 ex 
 |-  ( ch -> ( -. ph -> -. ( ( -. ph /\ -. ( -. ps /\ -. ch ) ) -> ( -. ch /\ -. ( -. ps /\ -. ph ) ) ) ) )
27 26 con4d 
 |-  ( ch -> ( ( ( -. ph /\ -. ( -. ps /\ -. ch ) ) -> ( -. ch /\ -. ( -. ps /\ -. ph ) ) ) -> ph ) )
28 27 com12 
 |-  ( ( ( -. ph /\ -. ( -. ps /\ -. ch ) ) -> ( -. ch /\ -. ( -. ps /\ -. ph ) ) ) -> ( ch -> ph ) )
29 17 28 anim12i 
 |-  ( ( ( ( -. ch /\ -. ( -. ps /\ -. ph ) ) -> ( -. ph /\ -. ( -. ps /\ -. ch ) ) ) /\ ( ( -. ph /\ -. ( -. ps /\ -. ch ) ) -> ( -. ch /\ -. ( -. ps /\ -. ph ) ) ) ) -> ( ( ph -> ch ) /\ ( ch -> ph ) ) )
30 dfbi2 
 |-  ( ( ( -. ch /\ -. ( -. ps /\ -. ph ) ) <-> ( -. ph /\ -. ( -. ps /\ -. ch ) ) ) <-> ( ( ( -. ch /\ -. ( -. ps /\ -. ph ) ) -> ( -. ph /\ -. ( -. ps /\ -. ch ) ) ) /\ ( ( -. ph /\ -. ( -. ps /\ -. ch ) ) -> ( -. ch /\ -. ( -. ps /\ -. ph ) ) ) ) )
31 dfbi2 
 |-  ( ( ph <-> ch ) <-> ( ( ph -> ch ) /\ ( ch -> ph ) ) )
32 29 30 31 3imtr4i 
 |-  ( ( ( -. ch /\ -. ( -. ps /\ -. ph ) ) <-> ( -. ph /\ -. ( -. ps /\ -. ch ) ) ) -> ( ph <-> ch ) )
33 6 32 impbii 
 |-  ( ( ph <-> ch ) <-> ( ( -. ch /\ -. ( -. ps /\ -. ph ) ) <-> ( -. ph /\ -. ( -. ps /\ -. ch ) ) ) )
34 norcom 
 |-  ( ( ( ph -\/ ps ) -\/ ch ) <-> ( ch -\/ ( ph -\/ ps ) ) )
35 df-nor 
 |-  ( ( ch -\/ ( ph -\/ ps ) ) <-> -. ( ch \/ ( ph -\/ ps ) ) )
36 ioran 
 |-  ( -. ( ch \/ ( ph -\/ ps ) ) <-> ( -. ch /\ -. ( ph -\/ ps ) ) )
37 norcom 
 |-  ( ( ph -\/ ps ) <-> ( ps -\/ ph ) )
38 df-nor 
 |-  ( ( ps -\/ ph ) <-> -. ( ps \/ ph ) )
39 ioran 
 |-  ( -. ( ps \/ ph ) <-> ( -. ps /\ -. ph ) )
40 37 38 39 3bitri 
 |-  ( ( ph -\/ ps ) <-> ( -. ps /\ -. ph ) )
41 40 notbii 
 |-  ( -. ( ph -\/ ps ) <-> -. ( -. ps /\ -. ph ) )
42 41 anbi2i 
 |-  ( ( -. ch /\ -. ( ph -\/ ps ) ) <-> ( -. ch /\ -. ( -. ps /\ -. ph ) ) )
43 36 42 bitri 
 |-  ( -. ( ch \/ ( ph -\/ ps ) ) <-> ( -. ch /\ -. ( -. ps /\ -. ph ) ) )
44 34 35 43 3bitri 
 |-  ( ( ( ph -\/ ps ) -\/ ch ) <-> ( -. ch /\ -. ( -. ps /\ -. ph ) ) )
45 df-nor 
 |-  ( ( ph -\/ ( ps -\/ ch ) ) <-> -. ( ph \/ ( ps -\/ ch ) ) )
46 ioran 
 |-  ( -. ( ph \/ ( ps -\/ ch ) ) <-> ( -. ph /\ -. ( ps -\/ ch ) ) )
47 df-nor 
 |-  ( ( ps -\/ ch ) <-> -. ( ps \/ ch ) )
48 ioran 
 |-  ( -. ( ps \/ ch ) <-> ( -. ps /\ -. ch ) )
49 47 48 bitri 
 |-  ( ( ps -\/ ch ) <-> ( -. ps /\ -. ch ) )
50 49 notbii 
 |-  ( -. ( ps -\/ ch ) <-> -. ( -. ps /\ -. ch ) )
51 50 anbi2i 
 |-  ( ( -. ph /\ -. ( ps -\/ ch ) ) <-> ( -. ph /\ -. ( -. ps /\ -. ch ) ) )
52 45 46 51 3bitri 
 |-  ( ( ph -\/ ( ps -\/ ch ) ) <-> ( -. ph /\ -. ( -. ps /\ -. ch ) ) )
53 44 52 bibi12i 
 |-  ( ( ( ( ph -\/ ps ) -\/ ch ) <-> ( ph -\/ ( ps -\/ ch ) ) ) <-> ( ( -. ch /\ -. ( -. ps /\ -. ph ) ) <-> ( -. ph /\ -. ( -. ps /\ -. ch ) ) ) )
54 33 53 bitr4i 
 |-  ( ( ph <-> ch ) <-> ( ( ( ph -\/ ps ) -\/ ch ) <-> ( ph -\/ ( ps -\/ ch ) ) ) )