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

Theorem isibcg 26294
 Description: The predicate "is an incidence betwenness geometry with congruences". (For my private use only. Don't use.) (Contributed by FL, 16-Sep-2016.)
Hypotheses
Ref Expression
isibcg.1 angc
isibcg.2 PPoints
isibcg.3 Segments
isibcg.4 btw
isibcg.5 ray
isibcg.6 segc
isibcg.7
isibcg.8
isibcg.9 Halfplane
isibcg.10 triangle
isibcg.11 angle
isibcg.12 trcng
isibcg.13 dWords
Assertion
Ref Expression
isibcg Ibcg Ibg
Distinct variable groups:   ,,,,,   , ,,,,   , ,,,,,   , ,,,,   ,,,,,,   ,,,,,,   ,,,,,   ,,,,,,   ,,,,,,   ,,,,,,   ,,,,,,   ,,,,,   ,,,,,   ,,,,,
Allowed substitution hints:   ()   ()   (,,,,,)   ()   ()   ()   ()

Proof of Theorem isibcg
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-ibcg 26293 . . 3 Ibcg Ibg angc PPoints btw ray segc angle triangle dWords Halfplane Segments trcng
21eleq2i 2360 . 2 Ibcg Ibg angc PPoints btw ray segc angle triangle dWords Halfplane Segments trcng
3 fveq2 5541 . . . 4 angc angc
4 fveq2 5541 . . . . 5 PPoints PPoints
5 fveq2 5541 . . . . . 6 btw btw
6 fveq2 5541 . . . . . . 7 ray ray
7 fveq2 5541 . . . . . . . 8 segc segc
8 fveq2 5541 . . . . . . . . 9
9 fveq2 5541 . . . . . . . . . 10
10 fveq2 5541 . . . . . . . . . . 11 angle angle
11 fveq2 5541 . . . . . . . . . . . 12 triangle triangle
12 fveq2 5541 . . . . . . . . . . . . . 14 Halfplane Halfplane
13 fveq2 5541 . . . . . . . . . . . . . . 15 Segments Segments
14 fveq2 5541 . . . . . . . . . . . . . . . 16 trcng trcng
15 biidd 228 . . . . . . . . . . . . . . . 16
1614, 15sbcbidv2 25072 . . . . . . . . . . . . . . 15 trcng trcng
1713, 16sbcbidv2 25072 . . . . . . . . . . . . . 14 Segments trcng Segments trcng
1812, 17sbcbidv2 25072 . . . . . . . . . . . . 13 Halfplane Segments trcng Halfplane Segments trcng
1918sbcbidv 3058 . . . . . . . . . . . 12 dWords Halfplane Segments trcng dWords Halfplane Segments trcng
2011, 19sbcbidv2 25072 . . . . . . . . . . 11 triangle dWords Halfplane Segments trcng triangle dWords Halfplane Segments trcng
2110, 20sbcbidv2 25072 . . . . . . . . . 10 angle triangle dWords Halfplane Segments trcng angle triangle dWords Halfplane Segments trcng
229, 21sbcbidv2 25072 . . . . . . . . 9 angle triangle dWords Halfplane Segments trcng angle triangle dWords Halfplane Segments trcng
238, 22sbcbidv2 25072 . . . . . . . 8 angle triangle dWords Halfplane Segments trcng angle triangle dWords Halfplane Segments trcng
247, 23sbcbidv2 25072 . . . . . . 7 segc angle triangle dWords Halfplane Segments trcng segc angle triangle dWords Halfplane Segments trcng
256, 24sbcbidv2 25072 . . . . . 6 ray segc angle triangle dWords Halfplane Segments trcng ray segc angle triangle dWords Halfplane Segments trcng
265, 25sbcbidv2 25072 . . . . 5 btw ray segc angle triangle dWords Halfplane Segments trcng btw ray segc angle triangle dWords Halfplane Segments trcng
274, 26sbcbidv2 25072 . . . 4 PPoints btw ray segc angle triangle dWords Halfplane Segments trcng PPoints btw ray segc angle triangle dWords Halfplane Segments trcng
283, 27sbcbidv2 25072 . . 3 angc PPoints btw ray segc angle triangle dWords Halfplane Segments trcng angc PPoints btw ray segc angle triangle dWords Halfplane Segments trcng
2928elrab 2936 . 2 Ibg angc PPoints btw ray segc angle triangle dWords Halfplane Segments trcng Ibg angc PPoints btw ray segc angle triangle dWords Halfplane Segments trcng
30 fvex 5555 . . . . . 6 angc
31 isibcg.1 . . . . . . 7 angc
32 eqtr 2313 . . . . . . . . . 10 angc angc
33 ereq1 6683 . . . . . . . . . . . . . . . . . . . . . . 23
34 breq 4041 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
3534reubidv 2737 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
3635ralbidv 2576 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
3736anbi1d 685 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
3837ralbidv 2576 . . . . . . . . . . . . . . . . . . . . . . . . . 26
3938anbi2d 684 . . . . . . . . . . . . . . . . . . . . . . . . 25
4039imbi2d 307 . . . . . . . . . . . . . . . . . . . . . . . 24
41402ralbidv 2598 . . . . . . . . . . . . . . . . . . . . . . 23
4233, 413anbi23d 1255 . . . . . . . . . . . . . . . . . . . . . 22
4342sbcbidv 3058 . . . . . . . . . . . . . . . . . . . . 21 trcng trcng
4443sbcbidv 3058 . . . . . . . . . . . . . . . . . . . 20 Segments trcng Segments trcng
4544sbcbidv 3058 . . . . . . . . . . . . . . . . . . 19 Halfplane Segments trcng Halfplane Segments trcng
4645sbcbidv 3058 . . . . . . . . . . . . . . . . . 18 dWords Halfplane Segments trcng dWords Halfplane Segments trcng
4746sbcbidv 3058 . . . . . . . . . . . . . . . . 17 triangle dWords Halfplane Segments trcng triangle dWords Halfplane Segments trcng
4847sbcbidv 3058 . . . . . . . . . . . . . . . 16 angle triangle dWords Halfplane Segments trcng angle triangle dWords Halfplane Segments trcng
4948sbcbidv 3058 . . . . . . . . . . . . . . 15 angle triangle dWords Halfplane Segments trcng angle triangle dWords Halfplane Segments trcng
5049sbcbidv 3058 . . . . . . . . . . . . . 14 angle triangle dWords Halfplane Segments trcng angle triangle dWords Halfplane Segments trcng
5150sbcbidv 3058 . . . . . . . . . . . . 13 segc angle triangle dWords Halfplane Segments trcng segc angle triangle dWords Halfplane Segments trcng
5251sbcbidv 3058 . . . . . . . . . . . 12 ray segc angle triangle dWords Halfplane Segments trcng ray segc angle triangle