Metamath Proof Explorer

Theorem mdoc2i

Description: Orthocomplements form a modular pair. (Contributed by NM, 29-Apr-2006) (New usage is discouraged.)

Ref Expression
Hypothesis mdoc1.1 
|- A e. CH
Assertion mdoc2i 
|- ( _|_ ` A ) MH A

Proof

Step Hyp Ref Expression
1 mdoc1.1 
 |-  A e. CH
2 1 choccli 
 |-  ( _|_ ` A ) e. CH
3 2 mdoc1i 
 |-  ( _|_ ` A ) MH ( _|_ ` ( _|_ ` A ) )
4 1 ococi 
 |-  ( _|_ ` ( _|_ ` A ) ) = A
5 3 4 breqtri 
 |-  ( _|_ ` A ) MH A