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

Theorem cvrnbtwn3 30074
 Description: The covers relation implies no in-betweenness. (cvnbtwn3 23791 analog.) (Contributed by NM, 4-Nov-2011.)
Hypotheses
Ref Expression
cvrletr.b
cvrletr.l
cvrletr.s
cvrletr.c
Assertion
Ref Expression
cvrnbtwn3

Proof of Theorem cvrnbtwn3
StepHypRef Expression
1 cvrletr.b . . . 4
2 cvrletr.s . . . 4
3 cvrletr.c . . . 4
41, 2, 3cvrnbtwn 30069 . . 3
5 cvrletr.l . . . . . . . . 9
65, 2pltval 14417 . . . . . . . 8
763adant3r2 1163 . . . . . . 7
873adant3 977 . . . . . 6
98anbi1d 686 . . . . 5
109notbid 286 . . . 4
11 an32 774 . . . . . . 7
12 df-ne 2601 . . . . . . . 8
1312anbi2i 676 . . . . . . 7
1411, 13bitri 241 . . . . . 6
1514notbii 288 . . . . 5
16 iman 414 . . . . 5
1715, 16bitr4i 244 . . . 4
1810, 17syl6bb 253 . . 3
194, 18mpbid 202 . 2
201, 5posref 14408 . . . . . 6
21 breq2 4216 . . . . . 6
2220, 21syl5ibcom 212 . . . . 5
23223ad2antr1 1122 . . . 4
25 simp1 957 . . . . 5
26 simp21 990 . . . . 5
27 simp22 991 . . . . 5
28 simp3 959 . . . . 5
291, 2, 3cvrlt 30068 . . . . 5
3025, 26, 27, 28, 29syl31anc 1187 . . . 4
31 breq1 4215 . . . 4
3230, 31syl5ibcom 212 . . 3