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

Theorem cvrnbtwn3 30148
 Description: The covers relation implies no in-betweenness. (cvnbtwn3 23796 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 30143 . . 3
5 cvrletr.l . . . . . . . . 9
65, 2pltval 14422 . . . . . . . 8
763adant3r2 1164 . . . . . . 7
873adant3 978 . . . . . 6
98anbi1d 687 . . . . 5
109notbid 287 . . . 4
11 an32 775 . . . . . . 7
12 df-ne 2603 . . . . . . . 8
1312anbi2i 677 . . . . . . 7
1411, 13bitri 242 . . . . . 6
1514notbii 289 . . . . 5
16 iman 415 . . . . 5
1715, 16bitr4i 245 . . . 4
1810, 17syl6bb 254 . . 3
194, 18mpbid 203 . 2
201, 5posref 14413 . . . . . 6
21 breq2 4219 . . . . . 6
2220, 21syl5ibcom 213 . . . . 5
23223ad2antr1 1123 . . . 4