Metamath Proof Explorer


Theorem acongtr

Description: Transitivity of alternating congruence. (Contributed by Stefan O'Rear, 2-Oct-2014)

Ref Expression
Assertion acongtr ABCDABCABCACDACDABDABD

Proof

Step Hyp Ref Expression
1 congtr ABCDABCACDABD
2 1 3expa ABCDABCACDABD
3 2 orcd ABCDABCACDABDABD
4 3 ex ABCDABCACDABDABD
5 simpll ABCDABCACDAB
6 znegcl CC
7 znegcl DD
8 6 7 anim12i CDCD
9 8 ad2antlr ABCDABCACDCD
10 simplll ABCDACDA
11 simplrl ABCDACDC
12 simplrr ABCDACDD
13 simpr ABCDACDACD
14 congsym ACDACDADC
15 10 11 12 13 14 syl22anc ABCDACDADC
16 15 ex ABCDACDADC
17 zcn CC
18 17 adantr CDC
19 zcn DD
20 19 adantl CDD
21 18 20 neg2subd CD-C-D=DC
22 21 adantl ABCD-C-D=DC
23 22 eqcomd ABCDDC=-C-D
24 23 breq2d ABCDADCA-C-D
25 16 24 sylibd ABCDACDA-C-D
26 25 anim2d ABCDABCACDABCA-C-D
27 26 imp ABCDABCACDABCA-C-D
28 congtr ABCDABCA-C-DABD
29 5 9 27 28 syl3anc ABCDABCACDABD
30 29 olcd ABCDABCACDABDABD
31 30 ex ABCDABCACDABDABD
32 simpll ABCDABCACDAB
33 7 anim2i CDCD
34 33 ad2antlr ABCDABCACDCD
35 simpr ABCDABCACDABCACD
36 congtr ABCDABCACDABD
37 32 34 35 36 syl3anc ABCDABCACDABD
38 37 olcd ABCDABCACDABDABD
39 38 ex ABCDABCACDABDABD
40 simpll ABCDABCACDAB
41 6 anim1i CDCD
42 41 ad2antlr ABCDABCACDCD
43 simpl ADA
44 simpr BCC
45 43 44 anim12i ADBCAC
46 45 an42s ABCDAC
47 46 adantr ABCDACDAC
48 7 adantl CDD
49 48 ad2antlr ABCDACDD
50 simpr ABCDACDACD
51 congsym ACDACDA-D-C
52 47 49 50 51 syl12anc ABCDACDA-D-C
53 52 ex ABCDACDA-D-C
54 18 negnegd CDC=C
55 54 oveq2d CD-D-C=-D-C
56 zcn CC
57 56 adantr CDC
58 8 57 syl CDC
59 20 58 neg2subd CD-D-C=-C-D
60 55 59 eqtr3d CD-D-C=-C-D
61 60 adantl ABCD-D-C=-C-D
62 61 breq2d ABCDA-D-CA-C-D
63 53 62 sylibd ABCDACDA-C-D
64 63 anim2d ABCDABCACDABCA-C-D
65 64 imp ABCDABCACDABCA-C-D
66 congtr ABCDABCA-C-DABD
67 40 42 65 66 syl3anc ABCDABCACDABD
68 67 orcd ABCDABCACDABDABD
69 68 ex ABCDABCACDABDABD
70 4 31 39 69 ccased ABCDABCABCACDACDABDABD
71 70 3impia ABCDABCABCACDACDABDABD