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 32545

Description: Variation of projective geometry axiom ps-2 32495. (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 1027	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $/\$ $.\/$
2		simp12 1028	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $/\$ $.\/$
3		simp21 1030	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $/\$ $.\/$
4		hllat 32381	. . . . 5
5	1, 4	syl 17	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $/\$ $.\/$
6		eqid 2402	. . . . . 6
7		2atm.a	. . . . . 6
8	6, 7	atbase 32307	. . . . 5
9	2, 8	syl 17	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $/\$ $.\/$
10		simp13 1029	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $/\$ $.\/$
11	6, 7	atbase 32307	. . . . 5
12	10, 11	syl 17	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $/\$ $.\/$
13	6, 7	atbase 32307	. . . . 5
14	3, 13	syl 17	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $/\$ $.\/$
15		simp31l 1120	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$
16		2atm.l	. . . . 5
17		2atm.j	. . . . 5 $.\/$
18	6, 16, 17	latnlej1r 16024	. . . 4 $/\$ $/\$ $/\$ $/\$ $.\/$
19	5, 9, 12, 14, 15, 18	syl131anc 1243	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $/\$ $.\/$
20		eqid 2402	. . . 4
21	17, 7, 20	llni2 32529	. . 3 $/\$ $/\$ $/\$ $.\/$
22	1, 2, 3, 19, 21	syl31anc 1233	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$
23		simp22 1031	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $/\$ $.\/$
24		simp23 1032	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $/\$ $.\/$
25		simp31r 1121	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $/\$ $.\/$
26	17, 7, 20	llni2 32529	. . 3 $/\$ $/\$ $/\$ $.\/$
27	1, 23, 24, 25, 26	syl31anc 1233	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$
28		simp32 1034	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$
29		simp33 1035	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$
30		2atm.m	. . . 4 $./\$
31		eqid 2402	. . . 4
32	16, 17, 30, 31, 7	ps-2b 32499	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $./\$ $.\/$
33	1, 2, 10, 3, 23, 24, 15, 25, 29, 32	syl333anc 1262	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $./\$ $.\/$
34	30, 31, 7, 20	2llnmat 32541	. 2 $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$
35	1, 22, 27, 28, 33, 34	syl32anc 1238	1 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $./\$ $.\/$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4 $/\$ wa 367 $/\$ w3a 974

wceq 1405

wcel 1842

wne 2598 class class class wbr 4395

cfv 5569 (class class class)co 6278

cbs 14841

cple 14916

cjn 15897

cmee 15898

cp0 15991

clat 15999

catm 32281

chlt 32368

clln 32508

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1639 ax-4 1652 ax-5 1725 ax-6 1771 ax-7 1814 ax-8 1844 ax-9 1846 ax-10 1861 ax-11 1866 ax-12 1878 ax-13 2026 ax-ext 2380 ax-rep 4507 ax-sep 4517 ax-nul 4525 ax-pow 4572 ax-pr 4630 ax-un 6574

This theorem depends on definitions: df-bi 185 df-or 368 df-an 369 df-3an 976 df-tru 1408 df-ex 1634 df-nf 1638 df-sb 1764 df-eu 2242 df-mo 2243 df-clab 2388 df-cleq 2394 df-clel 2397 df-nfc 2552 df-ne 2600 df-ral 2759 df-rex 2760 df-reu 2761 df-rab 2763 df-v 3061 df-sbc 3278 df-csb 3374 df-dif 3417 df-un 3419 df-in 3421 df-ss 3428 df-nul 3739 df-if 3886 df-pw 3957 df-sn 3973 df-pr 3975 df-op 3979 df-uni 4192 df-iun 4273 df-br 4396 df-opab 4454 df-mpt 4455 df-id 4738 df-xp 4829 df-rel 4830 df-cnv 4831 df-co 4832 df-dm 4833 df-rn 4834 df-res 4835 df-ima 4836 df-iota 5533 df-fun 5571 df-fn 5572 df-f 5573 df-f1 5574 df-fo 5575 df-f1o 5576 df-fv 5577 df-riota 6240 df-ov 6281 df-oprab 6282 df-preset 15881 df-poset 15899 df-plt 15912 df-lub 15928 df-glb 15929 df-join 15930 df-meet 15931 df-p0 15993 df-lat 16000 df-clat 16062 df-oposet 32194 df-ol 32196 df-oml 32197 df-covers 32284 df-ats 32285 df-atl 32316 df-cvlat 32340 df-hlat 32369 df-llines 32515

This theorem is referenced by: cdlemg18c 33699 dia2dimlem1 34084

W3C validator