Metamath Proof Explorer


Theorem shlej2

Description: Add disjunct to both sides of Hilbert subspace ordering. (Contributed by NM, 22-Jun-2004) (New usage is discouraged.)

Ref Expression
Assertion shlej2 ASBSCSABCACB

Proof

Step Hyp Ref Expression
1 shlej1 ASBSCSABACBC
2 shjcom ASCSAC=CA
3 2 3adant2 ASBSCSAC=CA
4 3 adantr ASBSCSABAC=CA
5 shjcom BSCSBC=CB
6 5 3adant1 ASBSCSBC=CB
7 6 adantr ASBSCSABBC=CB
8 1 4 7 3sstr3d ASBSCSABCACB