plibgax3 - Mathbox for Frédéric Liné

Mathbox for Frédéric Liné

< Previous Next >
Related theorems
Unicode version

Theorem plibgax3 15323

Description: The third axiom of a planar incidence-betweenness geometry.

**Hypothesis**
Ref	Expression
plibgax3.1

**Assertion**
Ref	Expression
plibgax3	$/\$ Plibg l l $/\$ l $/\$ l $/\$ $/\$ $/\$ $/\$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $/\$

Distinct variable groups:

,l,

**Proof of Theorem plibgax3**
Step	Hyp	Ref	Expression
1		plibgax3.1	. . . . . . 7
2		biid 187	. . . . . . 7 Plig $/\$ $/\$ $/\$ $/\$ $/\$ Plig $/\$ $/\$ $/\$ $/\$ $/\$
3		biid 187	. . . . . . 7 $/\$ l l $/\$ l $/\$ l $/\$ $/\$ $/\$ $/\$ l l $/\$ l $/\$ l $/\$ $/\$ $/\$
4		biid 187	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
5		biid 187	. . . . . . 7 l l $/\$ l $/\$ l $/\$ $/\$ $/\$ $/\$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $/\$ l l $/\$ l $/\$ l $/\$ $/\$ $/\$ $/\$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $/\$
6		biid 187	. . . . . . 7 l l $/\$ l $/\$ l $/\$ $\/$ $\/$ l $/\$ $\/$ $\/$ l $\/$ $\/$ l l l $/\$ l $/\$ l $/\$ $\/$ $\/$ l $/\$ $\/$ $\/$ l $\/$ $\/$ l
7		biid 187	. . . . . . 7 l l $/\$ l $/\$ l $/\$ $\/$ $\/$ l $/\$ $\/$ $\/$ l $\/$ $\/$ l l l $/\$ l $/\$ l $/\$ $\/$ $\/$ l $/\$ $\/$ $\/$ l $\/$ $\/$ l
8	1, 2, 3, 4, 5, 6, 7	isplibg 15319	. . . . . 6 $/\$ Plibg Plig $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ l l $/\$ l $/\$ l $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ l l $/\$ l $/\$ l $/\$ $/\$ $/\$ $/\$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $/\$ $/\$ l l $/\$ l $/\$ l $/\$ $\/$ $\/$ l $/\$ $\/$ $\/$ l $\/$ $\/$ l $/\$ l l $/\$ l $/\$ l $/\$ $\/$ $\/$ l $/\$ $\/$ $\/$ l $\/$ $\/$ l
9	8	simplbda 465	. . . . 5 $/\$ $/\$ Plibg $/\$ l l $/\$ l $/\$ l $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ l l $/\$ l $/\$ l $/\$ $/\$ $/\$ $/\$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $/\$ $/\$ l l $/\$ l $/\$ l $/\$ $\/$ $\/$ l $/\$ $\/$ $\/$ l $\/$ $\/$ l $/\$ l l $/\$ l $/\$ l $/\$ $\/$ $\/$ l $/\$ $\/$ $\/$ l $\/$ $\/$ l
10	9	simprd 352	. . . 4 $/\$ $/\$ Plibg $/\$ $/\$ $/\$ l l $/\$ l $/\$ l $/\$ $/\$ $/\$ $/\$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $/\$ $/\$ l l $/\$ l $/\$ l $/\$ $\/$ $\/$ l $/\$ $\/$ $\/$ l $\/$ $\/$ l $/\$ l l $/\$ l $/\$ l $/\$ $\/$ $\/$ l $/\$ $\/$ $\/$ l $\/$ $\/$ l
11	10	simprd 352	. . 3 $/\$ $/\$ Plibg l l $/\$ l $/\$ l $/\$ $/\$ $/\$ $/\$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $/\$ $/\$ l l $/\$ l $/\$ l $/\$ $\/$ $\/$ l $/\$ $\/$ $\/$ l $\/$ $\/$ l $/\$ l l $/\$ l $/\$ l $/\$ $\/$ $\/$ l $/\$ $\/$ $\/$ l $\/$ $\/$ l
12	11	simplld 348	. 2 $/\$ $/\$ Plibg l l $/\$ l $/\$ l $/\$ $/\$ $/\$ $/\$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $/\$
13	12	ex 402	1 $/\$ Plibg l l $/\$ l $/\$ l $/\$ $/\$ $/\$ $/\$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$ $/\$

Colors of variables: wff set class

Syntax hints:

wn 2

wi 3 $/\$ wa 240 $\/$ w3o 857 $/\$ w3a 858

wceq 1298

wcel 1300

wne 2017

wral 2105

wrex 2106

crab 2108

cin 2592

c0 2875

cop 3046

cuni 3177

cdm 3986

crn 3987

wrel 3991 Pligcplig 10343 Plibgcplibg 15295

This theorem was proved from axioms: ax-1 4 ax-2 5 ax-3 6 ax-mp 7 ax-7 1304 ax-gen 1305 ax-8 1306 ax-9 1307 ax-10 1308 ax-11 1309 ax-12 1310 ax-14 1312 ax-17 1317 ax-4 1319 ax-5o 1321 ax-6o 1324 ax-9o 1481 ax-10o 1500 ax-16 1580 ax-11o 1588 ax-ext 1865 ax-sep 3438 ax-nul 3445 ax-pow 3481 ax-pr 3524

This theorem depends on definitions: df-bi 164 df-or 241 df-an 242 df-3or 859 df-3an 860 df-ex 1327 df-sb 1536 df-eu 1775 df-mo 1776 df-clab 1872 df-cleq 1877 df-clel 1880 df-ne 2019 df-ral 2109 df-rex 2110 df-rab 2112 df-v 2294 df-dif 2597 df-un 2600 df-in 2603 df-ss 2605 df-nul 2876 df-pw 3035 df-sn 3049 df-pr 3050 df-op 3053 df-uni 3178 df-br 3339 df-opab 3396 df-rel 4001 df-cnv 4002 df-dm 4004 df-rn 4005 df-plibg0 15306 df-plibg1 15308 df-plibg2 15310 df-plibg3 15312 df-plibg4a 15314 df-plibg4b 15316 df-plibg 15318