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

Theorem dochord 32095
 Description: Ordering law for orthocomplement. (Contributed by NM, 12-Aug-2014.)
Hypotheses
Ref Expression
doch11.h
doch11.i
doch11.o
doch11.k
doch11.x
doch11.y
Assertion
Ref Expression
dochord

Proof of Theorem dochord
StepHypRef Expression
1 doch11.k . . . 4
3 doch11.y . . . . 5
4 doch11.h . . . . . 6
5 eqid 2435 . . . . . 6
6 doch11.i . . . . . 6
7 eqid 2435 . . . . . 6
84, 5, 6, 7dihrnss 32003 . . . . 5
91, 3, 8syl2anc 643 . . . 4
11 simpr 448 . . 3
12 doch11.o . . . 4
134, 5, 7, 12dochss 32090 . . 3
142, 10, 11, 13syl3anc 1184 . 2
151adantr 452 . . . 4
16 doch11.x . . . . . . . 8
174, 5, 6, 7dihrnss 32003 . . . . . . . 8
181, 16, 17syl2anc 643 . . . . . . 7
194, 6, 5, 7, 12dochcl 32078 . . . . . . 7
201, 18, 19syl2anc 643 . . . . . 6
214, 5, 6, 7dihrnss 32003 . . . . . 6
221, 20, 21syl2anc 643 . . . . 5
2322adantr 452 . . . 4
24 simpr 448 . . . 4
254, 5, 7, 12dochss 32090 . . . 4
2615, 23, 24, 25syl3anc 1184 . . 3
274, 6, 12dochoc 32092 . . . . 5
281, 16, 27syl2anc 643 . . . 4