Mathbox for Scott Fenton < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  ifscgr Unicode version

Theorem ifscgr 25706
 Description: Inner five segment congruence. Take two triangles, and , with between and and between and . If the other components of the triangles are congruent, then so are and . Theorem 4.2 of [Schwabhauser] p. 34. (Contributed by Scott Fenton, 27-Sep-2013.)
Assertion
Ref Expression
ifscgr Cgr

Proof of Theorem ifscgr
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 brifs 25705 . 2 Cgr Cgr Cgr Cgr
2 simp1l 981 . . . . . 6 Cgr Cgr Cgr Cgr
3 simp11 987 . . . . . . 7
4 simp13 989 . . . . . . 7
5 simp21 990 . . . . . . 7
6 axbtwnid 25606 . . . . . . 7
73, 4, 5, 6syl3anc 1184 . . . . . 6
82, 7syl5 30 . . . . 5 Cgr Cgr Cgr Cgr
9 simp2r 984 . . . . . . . . 9 Cgr Cgr Cgr Cgr Cgr
10 simp3r 986 . . . . . . . . 9 Cgr Cgr Cgr Cgr Cgr
119, 10jca 519 . . . . . . . 8 Cgr Cgr Cgr Cgr Cgr Cgr
12 opeq2 3941 . . . . . . . . . . 11
1312breq1d 4177 . . . . . . . . . 10 Cgr Cgr
14 opeq1 3940 . . . . . . . . . . 11
1514breq1d 4177 . . . . . . . . . 10 Cgr Cgr
1613, 15anbi12d 692 . . . . . . . . 9 Cgr Cgr Cgr Cgr
1716biimprd 215 . . . . . . . 8 Cgr Cgr Cgr Cgr
1811, 17mpan9 456 . . . . . . 7 Cgr Cgr Cgr Cgr Cgr Cgr
19 simp31 993 . . . . . . . . . 10
20 simp32 994 . . . . . . . . . 10
21 cgrid2 25665 . . . . . . . . . 10 Cgr
223, 4, 19, 20, 21syl13anc 1186 . . . . . . . . 9 Cgr
23 opeq1 3940 . . . . . . . . . . 11
2423breq2d 4179 . . . . . . . . . 10 Cgr Cgr
2524biimprd 215 . . . . . . . . 9 Cgr Cgr
2622, 25syl6 31 . . . . . . . 8 Cgr Cgr Cgr
2726imp3a 421 . . . . . . 7 Cgr Cgr Cgr
2818, 27syl5 30 . . . . . 6 Cgr Cgr Cgr Cgr Cgr
2928exp3a 426 . . . . 5 Cgr Cgr Cgr Cgr Cgr
308, 29mpdd 38 . . . 4 Cgr Cgr Cgr Cgr Cgr
31 opeq1 3940 . . . . . . . 8
3231breq2d 4179 . . . . . . 7
3332anbi1d 686 . . . . . 6
3431breq1d 4177 . . . . . . 7 Cgr Cgr
3534anbi1d 686 . . . . . 6 Cgr Cgr Cgr Cgr
3633, 353anbi12d 1255 . . . . 5 Cgr Cgr Cgr Cgr Cgr Cgr Cgr Cgr
3736imbi1d 309 . . . 4 Cgr Cgr Cgr Cgr Cgr Cgr Cgr Cgr Cgr Cgr
3830, 37syl5ibr 213 . . 3 Cgr Cgr Cgr Cgr Cgr
39 simp12 988 . . . . . . 7
40 btwndiff 25689 . . . . . . 7
413, 39, 5, 40syl3anc 1184 . . . . . 6
42 simpl11 1032 . . . . . . . . . 10
43 simpl23 1037 . . . . . . . . . 10
44 simpl32 1039 . . . . . . . . . 10
45 simpl21 1035 . . . . . . . . . 10
46 simpr 448 . . . . . . . . . 10
47 axsegcon 25594 . . . . . . . . . 10 Cgr
4842, 43, 44, 45, 46, 47syl122anc 1193 . . . . . . . . 9 Cgr
49 anass 631 . . . . . . . . . . . . 13 Cgr Cgr Cgr Cgr Cgr Cgr Cgr Cgr Cgr Cgr
50 anass 631 . . . . . . . . . . . . . 14 Cgr Cgr Cgr Cgr Cgr Cgr Cgr Cgr Cgr Cgr
51 simplrl 737 . . . . . . . . . . . . . . . . . . . . 21 Cgr Cgr Cgr Cgr Cgr
5251adantl 453 . . . . . . . . . . . . . . . . . . . 20 Cgr Cgr Cgr Cgr Cgr
53 simplll 735 . . . . . . . . . . . . . . . . . . . . 21 Cgr Cgr Cgr Cgr Cgr
5453adantl 453 . . . . . . . . . . . . . . . . . . . 20 Cgr Cgr Cgr Cgr Cgr
5552, 54jca 519 . . . . . . . . . . . . . . . . . . 19 Cgr Cgr Cgr Cgr Cgr
56 simpr2l 1016 . . . . . . . . . . . . . . . . . . . . 21 Cgr Cgr Cgr Cgr Cgr Cgr
5756adantl 453 . . . . . . . . . . . . . . . . . . . 20 Cgr Cgr Cgr Cgr Cgr Cgr
58 simpllr 736 . . . . . . . . . . . . . . . . . . . . . 22 Cgr Cgr Cgr Cgr Cgr Cgr
5958adantl 453 . . . . . . . . . . . . . . . . . . . . 21 Cgr Cgr Cgr Cgr Cgr Cgr
603ad2antrr 707 . . . . . . . . . . . . . . . . . . . . . 22 Cgr Cgr Cgr Cgr Cgr
6120ad2antrr 707 . . . . . . . . . . . . . . . . . . . . . 22 Cgr Cgr Cgr Cgr Cgr
62 simplrr 738 . . . . . . . . . . . . . . . . . . . . . 22 Cgr Cgr Cgr Cgr Cgr
635ad2antrr 707 . . . . . . . . . . . . . . . . . . . . . 22 Cgr Cgr Cgr Cgr Cgr
64 simplrl 737 . . . . . . . . . . . . . . . . . . . . . 22 Cgr Cgr Cgr Cgr Cgr
65 cgrcom 25652 . . . . . . . . . . . . . . . . . . . . . 22 Cgr Cgr
6660, 61, 62, 63, 64, 65syl122anc 1193 . . . . . . . . . . . . . . . . . . . . 21 Cgr Cgr Cgr Cgr Cgr Cgr Cgr
6759, 66mpbid 202 . . . . . . . . . . . . . . . . . . . 20 Cgr Cgr Cgr Cgr Cgr Cgr
6857, 67jca 519 . . . . . . . . . . . . . . . . . . 19 Cgr Cgr Cgr Cgr Cgr Cgr Cgr
69 simprr3 1007 . . . . . . . . . . . . . . . . . . 19 Cgr Cgr Cgr Cgr Cgr Cgr Cgr
7055, 68, 693jca 1134 . . . . . . . . . . . . . . . . . 18 Cgr Cgr Cgr Cgr Cgr Cgr Cgr Cgr Cgr
7170ex 424 . . . . . . . . . . . . . . . . 17 Cgr Cgr Cgr Cgr Cgr Cgr Cgr Cgr Cgr
72 simpl11 1032 . . . . . . . . . . . . . . . . . 18
73 simpl12 1033 . . . . . . . . . . . . . . . . . 18
74 simpl21 1035 . . . . . . . . . . . . . . . . . 18
75 simprl 733 . . . . . . . . . . . . . . . . . 18
76 simpl22 1036 . . . . . . . . . . . . . . . . . 18
77 simpl23 1037 . . . . . . . . . . . . . . . . . 18
78 simpl32 1039 . . . . . . . . . . . . . . . . . 18
79 simprr 734 . . . . . . . . . . . . . . . . . 18
80 simpl33 1040 . . . . . . . . . . . . . . . . . 18
81 brofs 25667 . . . . . . . . . . . . . . . . . 18 Cgr Cgr Cgr Cgr
8272, 73, 74, 75, 76, 77, 78, 79, 80, 81syl333anc 1216 . . . . . . . . . . . . . . . . 17 Cgr Cgr Cgr Cgr
8371, 82sylibrd 226 . . . . . . . . . . . . . . . 16 Cgr Cgr Cgr Cgr Cgr
84 5segofs 25668 . . . . . . . . . . . . . . . . 17 Cgr
8572, 73, 74, 75, 76, 77, 78, 79, 80, 84syl333anc 1216 . . . . . . . . . . . . . . . 16 Cgr
8683, 85syland 468 . . . . . . . . . . . . . . 15 Cgr Cgr Cgr Cgr Cgr Cgr
87 simpr1l 1014 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 Cgr Cgr Cgr Cgr Cgr
8887adantr 452 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 Cgr Cgr Cgr Cgr Cgr Cgr
8951adantr 452 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 Cgr Cgr Cgr Cgr Cgr Cgr
9088, 89jca 519 . . . . . . . . . . . . . . . . . . . . . . . . . 26 Cgr Cgr Cgr Cgr Cgr Cgr
91 simpr1r 1015 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 Cgr Cgr Cgr Cgr Cgr
9291adantr 452 . . . . . . . . . . . . . . . . . . . . . . . . . 26 Cgr Cgr Cgr Cgr Cgr Cgr
9353adantr 452 . . . . . . . . . . . . . . . . . . . . . . . . . 26 Cgr Cgr Cgr Cgr Cgr Cgr
9490, 92, 93jca32 522 . . . . . . . . . . . . . . . . . . . . . . . . 25 Cgr Cgr Cgr Cgr Cgr Cgr
95 simpl13 1034 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
96 btwnexch3 25682 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
9772, 73, 95, 74, 75, 96syl122anc 1193 . . . . . . . . . . . . . . . . . . . . . . . . . 26
98 simpl31 1038 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
99 btwnexch3 25682 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
10072, 77, 98, 78, 79, 99syl122anc 1193 . . . . . . . . . . . . . . . . . . . . . . . . . 26
10197, 100anim12d 547 . . . . . . . . . . . . . . . . . . . . . . . . 25
10294, 101syl5 30 . . . . . . . . . . . . . . . . . . . . . . . 24 Cgr Cgr Cgr Cgr Cgr Cgr
103102imp 419 . . . . . . . . . . . . . . . . . . . . . . 23 Cgr Cgr Cgr Cgr Cgr Cgr
104 btwncom 25676 . . . . . . . . . . . . . . . . . . . . . . . . . 26
10572, 74, 95, 75, 104syl13anc 1186 . . . . . . . . . . . . . . . . . . . . . . . . 25
106 btwncom 25676 . . . . . . . . . . . . . . . . . . . . . . . . . 26
10772, 78, 98, 79, 106syl13anc 1186 . . . . . . . . . . . . . . . . . . . . . . . . 25
108105, 107anbi12d 692 . . . . . . . . . . . . . . . . . . . . . . . 24
109108adantr 452 . . . . . . . . . . . . . . . . . . . . . . 23 Cgr Cgr Cgr Cgr Cgr Cgr
110103, 109mpbid 202 . . . . . . . . . . . . . . . . . . . . . 22 Cgr Cgr Cgr Cgr Cgr Cgr
11158ad2antrl 709 . . . . . . . . . . . . . . . . . . . . . . . 24 Cgr Cgr Cgr Cgr Cgr Cgr Cgr
11272, 78, 79, 74, 75, 65syl122anc 1193 . . . . . . . . . . . . . . . . . . . . . . . . . 26 Cgr Cgr
113 cgrcomlr 25660 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 Cgr Cgr
11472, 74, 75, 78, 79, 113syl122anc 1193 . . . . . . . . . . . . . . . . . . . . . . . . . 26 Cgr Cgr
115112, 114bitrd 245 . . . . . . . . . . . . . . . . . . . . . . . . 25 Cgr Cgr
116115adantr 452 . . . . . . . . . . . . . . . . . . . . . . . 24 Cgr Cgr Cgr Cgr Cgr Cgr Cgr Cgr
117111, 116mpbid 202 . . . . . . . . . . . . . . . . . . . . . . 23 Cgr Cgr Cgr Cgr Cgr Cgr Cgr
118 simpr2r 1017 . . . . . . . . . . . . . . . . . . . . . . . . 25 Cgr Cgr Cgr Cgr Cgr Cgr
119118ad2antrl 709 . . . . . . . . . . . . . . . . . . . . . . . 24 Cgr Cgr Cgr Cgr Cgr Cgr Cgr
12072, 95, 74, 98, 78, 119cgrcomlrand 25663 . . . . . . . . . . . . . . . . . . . . . . 23 Cgr Cgr Cgr Cgr Cgr Cgr Cgr
121117, 120jca 519 . . . . . . . . . . . . . . . . . . . . . 22 Cgr Cgr Cgr Cgr Cgr Cgr Cgr Cgr
122 simprr 734 . . . . . . . . . . . . . . . . . . . . . . 23 Cgr Cgr Cgr Cgr Cgr Cgr Cgr
123 simpr3r 1019 . . . . . . . . . . . . . . . . . . . . . . . 24 Cgr Cgr Cgr Cgr Cgr Cgr
124123ad2antrl 709 . . . . . . . . . . . . . . . . . . . . . . 23 Cgr Cgr Cgr Cgr Cgr Cgr Cgr
125122, 124jca 519 . . . . . . . . . . . . . . . . . . . . . 22 Cgr Cgr Cgr Cgr Cgr Cgr