ps-2b - Mathbox for Norm Megill

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

Theorem ps-2b 32499

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

**Hypotheses**
Ref	Expression
ps-2b.l
ps-2b.j	$.\/$
ps-2b.m	$./\$
ps-2b.z
ps-2b.a

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

Proof of Theorem ps-2b Dummy variable

is distinct from all other variables.

Step	Hyp	Ref	Expression
1		simp11 1027	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $/\$ $.\/$
2		simp12 1028	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $/\$ $.\/$
3		simp13 1029	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $/\$ $.\/$
4		simp21 1030	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $/\$ $.\/$
5	2, 3, 4	3jca 1177	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$
6		simp22 1031	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $/\$ $.\/$
7		simp23 1032	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $/\$ $.\/$
8	6, 7	jca 530	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$
9		simp31 1033	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$
10		simp32 1034	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $/\$ $.\/$
11	9, 10	jca 530	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$
12		simp33 1035	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$
13		ps-2b.l	. . . 4
14		ps-2b.j	. . . 4 $.\/$
15		ps-2b.a	. . . 4
16	13, 14, 15	ps-2 32495	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$
17	1, 5, 8, 11, 12, 16	syl32anc 1238	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$
18		simp111 1126	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $/\$ $.\/$
19		hlatl 32378	. . . . 5
20	18, 19	syl 17	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $/\$ $.\/$
21		hllat 32381	. . . . . 6
22	18, 21	syl 17	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $/\$ $.\/$
23		simp112 1127	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $/\$ $.\/$
24		simp121 1129	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $/\$ $.\/$
25		eqid 2402	. . . . . . 7
26	25, 14, 15	hlatjcl 32384	. . . . . 6 $/\$ $/\$ $.\/$
27	18, 23, 24, 26	syl3anc 1230	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$
28		simp122 1130	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $/\$ $.\/$
29		simp123 1131	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $/\$ $.\/$
30	25, 14, 15	hlatjcl 32384	. . . . . 6 $/\$ $/\$ $.\/$
31	18, 28, 29, 30	syl3anc 1230	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$
32		ps-2b.m	. . . . . 6 $./\$
33	25, 32	latmcl 16006	. . . . 5 $/\$ $.\/$ $/\$ $.\/$ $.\/$ $./\$ $.\/$
34	22, 27, 31, 33	syl3anc 1230	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $./\$ $.\/$
35		simp2 998	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $/\$ $.\/$
36		simp3 999	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$
37	25, 15	atbase 32307	. . . . . . 7
38	35, 37	syl 17	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $/\$ $.\/$
39	25, 13, 32	latlem12 16032	. . . . . 6 $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $./\$ $.\/$
40	22, 38, 27, 31, 39	syl13anc 1232	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $./\$ $.\/$
41	36, 40	mpbid 210	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $./\$ $.\/$
42		ps-2b.z	. . . . 5
43	25, 13, 42, 15	atlen0 32328	. . . 4 $/\$ $.\/$ $./\$ $.\/$ $/\$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$
44	20, 34, 35, 41, 43	syl31anc 1233	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $./\$ $.\/$
45	44	rexlimdv3a 2898	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $./\$ $.\/$
46	17, 45	mpd 15	1 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $./\$ $.\/$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 184 $/\$ wa 367 $/\$ w3a 974

wceq 1405

wcel 1842

wne 2598

wrex 2755 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

cal 32282

chlt 32368

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

This theorem is referenced by: ps-2c 32545

W3C validator