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

Theorem cdlemg31c 31433
 Description: Show that when is an atom, it is not under . TODO: Is there a shorter direct proof? Todo: should we eliminate here? (Contributed by NM, 29-May-2013.)
Hypotheses
Ref Expression
cdlemg12.l
cdlemg12.j
cdlemg12.m
cdlemg12.a
cdlemg12.h
cdlemg12.t
cdlemg12b.r
cdlemg31.n
Assertion
Ref Expression
cdlemg31c

Proof of Theorem cdlemg31c
StepHypRef Expression
1 simp11l 1068 . . . 4
2 simp11r 1069 . . . 4
31, 2jca 519 . . 3
4 simp13 989 . . 3
5 simp31 993 . . . 4
65necomd 2681 . . 3
7 simp12 988 . . . 4
8 simp2r 984 . . . 4
9 simp32 994 . . . 4
10 cdlemg12.l . . . . 5
11 cdlemg12.a . . . . 5
12 cdlemg12.h . . . . 5
13 cdlemg12.t . . . . 5
14 cdlemg12b.r . . . . 5
1510, 11, 12, 13, 14trlat 30903 . . . 4
163, 7, 8, 9, 15syl112anc 1188 . . 3
1710, 12, 13, 14trlle 30918 . . . 4
183, 8, 17syl2anc 643 . . 3
19 simp2l 983 . . 3
20 cdlemg12.j . . . 4
2110, 20, 11, 12lhp2atnle 30767 . . 3
223, 4, 6, 16, 18, 19, 21syl321anc 1206 . 2
23 simp12l 1070 . . . . . 6
24 simp13l 1072 . . . . . 6
25 simp2ll 1024 . . . . . 6
26 cdlemg12.m . . . . . . 7
27 cdlemg31.n . . . . . . 7
2810, 20, 26, 11, 12, 13, 14, 27cdlemg31a 31431 . . . . . 6
291, 2, 23, 24, 25, 8, 28syl222anc 1200 . . . . 5
3029adantr 452 . . . 4
31 simp111 1086 . . . . . . 7
32 simp112 1087 . . . . . . 7
33 simp3 959 . . . . . . . 8
3433necomd 2681 . . . . . . 7
35 simp12l 1070 . . . . . . 7
36 simp133 1094 . . . . . . 7
37 simp2 958 . . . . . . 7
3810, 20, 11, 12lhp2atnle 30767 . . . . . . 7
3931, 32, 34, 35, 36, 37, 38syl312anc 1205 . . . . . 6
40393expia 1155 . . . . 5
4140necon4ad 2659 . . . 4
4230, 41mpd 15 . . 3
4310, 20, 26, 11, 12, 13, 14, 27cdlemg31b 31432 . . . . 5
441, 2, 23, 24, 25, 8, 43syl222anc 1200 . . . 4