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

Theorem dalem52 35150
 Description: Lemma for dath 35162. Lines and intersect at an atom. (Contributed by NM, 8-Aug-2012.)
Hypotheses
Ref Expression
dalem.ph
dalem.l
dalem.j
dalem.a
dalem.ps
dalem44.m
dalem44.o
dalem44.y
dalem44.z
dalem44.g
dalem44.h
dalem44.i
Assertion
Ref Expression
dalem52

Proof of Theorem dalem52
StepHypRef Expression
1 dalem.ph . . . . 5
21dalemkehl 35049 . . . 4
4 dalem.ps . . . . 5
5 dalem.a . . . . 5
64, 5dalemcceb 35115 . . . 4
83, 7jca 532 . 2
9 dalem.l . . . 4
10 dalem.j . . . 4
11 dalem44.m . . . 4
12 dalem44.o . . . 4
13 dalem44.y . . . 4
14 dalem44.z . . . 4
15 dalem44.g . . . 4
161, 9, 10, 5, 4, 11, 12, 13, 14, 15dalem23 35122 . . 3
17 dalem44.h . . . 4
181, 9, 10, 5, 4, 11, 12, 13, 14, 17dalem29 35127 . . 3
19 dalem44.i . . . 4
201, 9, 10, 5, 4, 11, 12, 13, 14, 19dalem34 35132 . . 3
2116, 18, 203jca 1175 . 2
221dalempea 35052 . . . 4
231dalemqea 35053 . . . 4
241dalemrea 35054 . . . 4
2522, 23, 243jca 1175 . . 3
271, 9, 10, 5, 4, 11, 12, 13, 14, 15, 17, 19dalem42 35140 . 2
281dalemyeo 35058 . . 3
301, 9, 10, 5, 4, 11, 12, 13, 14, 15, 17, 19dalem45 35143 . . 3
311, 9, 10, 5, 4, 11, 12, 13, 14, 15, 17, 19dalem46 35144 . . 3
321, 9, 10, 5, 4, 11, 12, 13, 14, 15, 17, 19dalem47 35145 . . 3
3330, 31, 323jca 1175 . 2
341, 9, 10, 5, 4, 11, 12, 13, 14, 15, 17, 19dalem48 35146 . . . 4
351, 9, 10, 5, 4, 11, 12, 13, 14, 15, 17, 19dalem49 35147 . . . 4
361, 9, 10, 5, 4, 11, 12, 13, 14, 15, 17, 19dalem50 35148 . . . 4
3734, 35, 363jca 1175 . . 3