Theorem mdoc1i

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

	Ref	Expression
Hypothesis	mdoc1.1	⊢ 𝐴 ∈ Cℋ
Assertion	mdoc1i	⊢ 𝐴 𝑀ℋ ( ⊥ ‘ 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		mdoc1.1	⊢ 𝐴 ∈ Cℋ
2	1	cmidi	⊢ 𝐴 𝐶ℋ 𝐴
3	1 1 2	cmcm2ii	⊢ 𝐴 𝐶ℋ ( ⊥ ‘ 𝐴 )
4	1	choccli	⊢ ( ⊥ ‘ 𝐴 ) ∈ Cℋ
5	1 4	cmmdi	⊢ ( 𝐴 𝐶ℋ ( ⊥ ‘ 𝐴 ) → 𝐴 𝑀ℋ ( ⊥ ‘ 𝐴 ) )
6	3 5	ax-mp	⊢ 𝐴 𝑀ℋ ( ⊥ ‘ 𝐴 )