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

Definition df-angtrg 25553
 Description: Select an angle in a triangle. Definition 2 of [AitkenIBCG] p. 3. (Contributed by FL, 2-Sep-2016.)
Assertion
Ref Expression
df-angtrg angtrg Ig PPointsdWords angle
Distinct variable group:   ,,

Detailed syntax breakdown of Definition df-angtrg
StepHypRef Expression
1 cangtrg 25552 . 2 angtrg
2 vg . . 3
3 cig 25427 . . 3 Ig
4 vu . . . 4
5 vx . . . 4
62cv 1618 . . . . . 6
7 cpoints 25423 . . . . . 6 PPoints
86, 7cfv 4673 . . . . 5 PPoints
9 c3 9764 . . . . 5
10 cdwords 25351 . . . . 5 dWords
118, 9, 10co 5792 . . . 4 PPointsdWords
12 c1 8706 . . . . 5
13 cfz 10748 . . . . 5
1412, 9, 13co 5792 . . . 4
155cv 1618 . . . . . . 7
16 c2 9763 . . . . . . 7
1715, 16wceq 1619 . . . . . 6
184cv 1618 . . . . . . . 8
1912, 18cfv 4673 . . . . . . 7
2016, 18cfv 4673 . . . . . . 7
219, 18cfv 4673 . . . . . . 7
2219, 20, 21cs3 11457 . . . . . 6
2315, 9wceq 1619 . . . . . . 7
2420, 21, 19cs3 11457 . . . . . . 7
2521, 19, 20cs3 11457 . . . . . . 7
2623, 24, 25cif 3539 . . . . . 6
2717, 22, 26cif 3539 . . . . 5
28 cangle 25524 . . . . . 6 angle
296, 28cfv 4673 . . . . 5 angle
3027, 29cfv 4673 . . . 4 angle
314, 5, 11, 14, 30cmpt2 5794 . . 3 PPointsdWords angle
322, 3, 31cmpt 4051 . 2 Ig PPointsdWords angle
331, 32wceq 1619 1 angtrg Ig PPointsdWords angle
 Colors of variables: wff set class
 Copyright terms: Public domain W3C validator