Metamath Proof Explorer


Theorem shlej2i

Description: Add disjunct to both sides of Hilbert subspace ordering. (Contributed by NM, 19-Oct-1999) (New usage is discouraged.)

Ref Expression
Hypotheses shincl.1 AS
shincl.2 BS
shless.1 CS
Assertion shlej2i ABCACB

Proof

Step Hyp Ref Expression
1 shincl.1 AS
2 shincl.2 BS
3 shless.1 CS
4 1 2 3 shlej1i ABACBC
5 3 1 shjcomi CA=AC
6 3 2 shjcomi CB=BC
7 4 5 6 3sstr4g ABCACB