Metamath Proof Explorer

Theorem mdoc1i

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 mdoc1i 
|- A MH ( _|_ ` A )

Proof

Step Hyp Ref Expression
1 mdoc1.1 
 |-  A e. CH
2 1 cmidi 
 |-  A C_H A
3 1 1 2 cmcm2ii 
 |-  A C_H ( _|_ ` A )
4 1 choccli 
 |-  ( _|_ ` A ) e. CH
5 1 4 cmmdi 
 |-  ( A C_H ( _|_ ` A ) -> A MH ( _|_ ` A ) )
6 3 5 ax-mp 
 |-  A MH ( _|_ ` A )