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

Theorem cvrval2 29973
 Description: Binary relation expressing covers . Definition of covers in [Kalmbach] p. 15. (cvbr2 23776 analog.) (Contributed by NM, 16-Nov-2011.)
Hypotheses
Ref Expression
cvrletr.b
cvrletr.l
cvrletr.s
cvrletr.c
Assertion
Ref Expression
cvrval2
Distinct variable groups:   ,   ,   ,   ,   ,
Allowed substitution hints:   ()   ()   ()

Proof of Theorem cvrval2
StepHypRef Expression
1 cvrletr.b . . 3
2 cvrletr.s . . 3
3 cvrletr.c . . 3
41, 2, 3cvrval 29968 . 2
5 iman 414 . . . . . . . 8
6 df-ne 2600 . . . . . . . . 9
76anbi2i 676 . . . . . . . 8
85, 7xchbinxr 303 . . . . . . 7
9 cvrletr.l . . . . . . . . . . . . 13
109, 2pltval 14407 . . . . . . . . . . . 12
11103com23 1159 . . . . . . . . . . 11
12113expa 1153 . . . . . . . . . 10
1312anbi2d 685 . . . . . . . . 9
14 anass 631 . . . . . . . . 9
1513, 14syl6rbbr 256 . . . . . . . 8
1615notbid 286 . . . . . . 7
178, 16syl5bb 249 . . . . . 6
1817ralbidva 2713 . . . . 5
19 ralnex 2707 . . . . 5
2018, 19syl6bb 253 . . . 4
2120anbi2d 685 . . 3