ps-2c - Mathbox for Norm Megill

	Mathbox for Norm Megill	< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > ps-2c		Structured version Unicode version

Theorem ps-2c 33491

Description: Variation of projective geometry axiom ps-2 33441. (Contributed by NM, 3-Jul-2012.)

**Hypotheses**
Ref	Expression
2atm.l
2atm.j	$.\/$
2atm.m	$./\$
2atm.a

**Assertion**
Ref	Expression
ps-2c	$/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $./\$ $.\/$

**Proof of Theorem ps-2c**
Step	Hyp	Ref	Expression
1		simp11 1018	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $/\$ $.\/$
2		simp12 1019	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $/\$ $.\/$
3		simp21 1021	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $/\$ $.\/$
4		hllat 33327	. . . . 5
5	1, 4	syl 16	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $/\$ $.\/$
6		eqid 2452	. . . . . 6
7		2atm.a	. . . . . 6
8	6, 7	atbase 33253	. . . . 5
9	2, 8	syl 16	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $/\$ $.\/$
10		simp13 1020	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $/\$ $.\/$
11	6, 7	atbase 33253	. . . . 5
12	10, 11	syl 16	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $/\$ $.\/$
13	6, 7	atbase 33253	. . . . 5
14	3, 13	syl 16	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $/\$ $.\/$
15		simp31l 1111	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$
16		2atm.l	. . . . 5
17		2atm.j	. . . . 5 $.\/$
18	6, 16, 17	latnlej1r 15354	. . . 4 $/\$ $/\$ $/\$ $/\$ $.\/$
19	5, 9, 12, 14, 15, 18	syl131anc 1232	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $/\$ $.\/$
20		eqid 2452	. . . 4
21	17, 7, 20	llni2 33475	. . 3 $/\$ $/\$ $/\$ $.\/$
22	1, 2, 3, 19, 21	syl31anc 1222	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$
23		simp22 1022	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $/\$ $.\/$
24		simp23 1023	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $/\$ $.\/$
25		simp31r 1112	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $/\$ $.\/$
26	17, 7, 20	llni2 33475	. . 3 $/\$ $/\$ $/\$ $.\/$
27	1, 23, 24, 25, 26	syl31anc 1222	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$
28		simp32 1025	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$
29		simp33 1026	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$
30		2atm.m	. . . 4 $./\$
31		eqid 2452	. . . 4
32	16, 17, 30, 31, 7	ps-2b 33445	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $./\$ $.\/$
33	1, 2, 10, 3, 23, 24, 15, 25, 29, 32	syl333anc 1251	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $./\$ $.\/$
34	30, 31, 7, 20	2llnmat 33487	. 2 $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$
35	1, 22, 27, 28, 33, 34	syl32anc 1227	1 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $./\$ $.\/$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4 $/\$ wa 369 $/\$ w3a 965

wceq 1370

wcel 1758

wne 2645 class class class wbr 4395

cfv 5521 (class class class)co 6195

cbs 14287

cple 14359

cjn 15228

cmee 15229

cp0 15321

clat 15329

catm 33227

chlt 33314

clln 33454

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1592 ax-4 1603 ax-5 1671 ax-6 1710 ax-7 1730 ax-8 1760 ax-9 1762 ax-10 1777 ax-11 1782 ax-12 1794 ax-13 1954 ax-ext 2431 ax-rep 4506 ax-sep 4516 ax-nul 4524 ax-pow 4573 ax-pr 4634 ax-un 6477

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3an 967 df-tru 1373 df-ex 1588 df-nf 1591 df-sb 1703 df-eu 2265 df-mo 2266 df-clab 2438 df-cleq 2444 df-clel 2447 df-nfc 2602 df-ne 2647 df-ral 2801 df-rex 2802 df-reu 2803 df-rab 2805 df-v 3074 df-sbc 3289 df-csb 3391 df-dif 3434 df-un 3436 df-in 3438 df-ss 3445 df-nul 3741 df-if 3895 df-pw 3965 df-sn 3981 df-pr 3983 df-op 3987 df-uni 4195 df-iun 4276 df-br 4396 df-opab 4454 df-mpt 4455 df-id 4739 df-xp 4949 df-rel 4950 df-cnv 4951 df-co 4952 df-dm 4953 df-rn 4954 df-res 4955 df-ima 4956 df-iota 5484 df-fun 5523 df-fn 5524 df-f 5525 df-f1 5526 df-fo 5527 df-f1o 5528 df-fv 5529 df-riota 6156 df-ov 6198 df-oprab 6199 df-poset 15230 df-plt 15242 df-lub 15258 df-glb 15259 df-join 15260 df-meet 15261 df-p0 15323 df-lat 15330 df-clat 15392 df-oposet 33140 df-ol 33142 df-oml 33143 df-covers 33230 df-ats 33231 df-atl 33262 df-cvlat 33286 df-hlat 33315 df-llines 33461

This theorem is referenced by: cdlemg18c 34643 dia2dimlem1 35028

W3C validator