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

Theorem lhp2atnle 30904
 Description: Inequality for 2 different atoms under co-atom . (Contributed by NM, 17-Jun-2013.)
Hypotheses
Ref Expression
lhp2atnle.l
lhp2atnle.j
lhp2atnle.a
lhp2atnle.h
Assertion
Ref Expression
lhp2atnle

Proof of Theorem lhp2atnle
StepHypRef Expression
1 simp11l 1069 . . . 4
2 hlatl 30232 . . . 4
31, 2syl 16 . . 3
4 simp3l 986 . . 3
5 eqid 2438 . . . 4
6 lhp2atnle.a . . . 4
75, 6atn0 30180 . . 3
83, 4, 7syl2anc 644 . 2
9 hllat 30235 . . . . . 6
101, 9syl 16 . . . . 5
11 eqid 2438 . . . . . . 7
1211, 6atbase 30161 . . . . . 6
134, 12syl 16 . . . . 5
14 simp12l 1071 . . . . . 6
15 simp2l 984 . . . . . 6
16 lhp2atnle.j . . . . . . 7
1711, 16, 6hlatjcl 30238 . . . . . 6
181, 14, 15, 17syl3anc 1185 . . . . 5
19 lhp2atnle.l . . . . . 6
20 eqid 2438 . . . . . 6
2111, 19, 20latleeqm2 14514 . . . . 5
2210, 13, 18, 21syl3anc 1185 . . . 4
23 lhp2atnle.h . . . . . 6
2419, 16, 20, 5, 6, 23lhp2at0 30903 . . . . 5
25 eqeq1 2444 . . . . 5
2624, 25syl5ibcom 213 . . . 4
2722, 26sylbid 208 . . 3