Mathbox for Frédéric Liné < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-segtrg Unicode version

Definition df-segtrg 26291
 Description: Select a segment in a triangle. (Contributed by FL, 2-Sep-2016.)
Assertion
Ref Expression
df-segtrg segtrg Ig PPointsdWords angle
Distinct variable group:   ,,

Detailed syntax breakdown of Definition df-segtrg
StepHypRef Expression
1 csegtrg 26290 . 2 segtrg
2 vg . . 3
3 cig 26163 . . 3 Ig
4 vu . . . 4
5 vx . . . 4
62cv 1631 . . . . . 6
7 cpoints 26159 . . . . . 6 PPoints
86, 7cfv 5271 . . . . 5 PPoints
9 c3 9812 . . . . 5
10 cdwords 26087 . . . . 5 dWords
118, 9, 10co 5874 . . . 4 PPointsdWords
12 c1 8754 . . . . 5
13 cfz 10798 . . . . 5
1412, 9, 13co 5874 . . . 4
155cv 1631 . . . . . . 7
1615, 12wceq 1632 . . . . . 6
174cv 1631 . . . . . . . 8
1812, 17cfv 5271 . . . . . . 7
19 c2 9811 . . . . . . . 8
2019, 17cfv 5271 . . . . . . 7
21 cseg 26233 . . . . . . . 8
226, 21cfv 5271 . . . . . . 7
2318, 20, 22co 5874 . . . . . 6
2415, 19wceq 1632 . . . . . . 7
259, 17cfv 5271 . . . . . . . 8
2620, 25, 22co 5874 . . . . . . 7
2725, 18, 22co 5874 . . . . . . 7
2824, 26, 27cif 3578 . . . . . 6
2916, 23, 28cif 3578 . . . . 5
30 cangle 26260 . . . . . 6 angle
316, 30cfv 5271 . . . . 5 angle
3229, 31cfv 5271 . . . 4 angle
334, 5, 11, 14, 32cmpt2 5876 . . 3 PPointsdWords angle
342, 3, 33cmpt 4093 . 2 Ig PPointsdWords angle
351, 34wceq 1632 1 segtrg Ig PPointsdWords angle
 Colors of variables: wff set class
 Copyright terms: Public domain W3C validator