Metamath Proof Explorer


Theorem shlej1i

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

Ref Expression
Hypotheses shincl.1 𝐴S
shincl.2 𝐵S
shless.1 𝐶S
Assertion shlej1i ( 𝐴𝐵 → ( 𝐴 𝐶 ) ⊆ ( 𝐵 𝐶 ) )

Proof

Step Hyp Ref Expression
1 shincl.1 𝐴S
2 shincl.2 𝐵S
3 shless.1 𝐶S
4 shlej1 ( ( ( 𝐴S𝐵S𝐶S ) ∧ 𝐴𝐵 ) → ( 𝐴 𝐶 ) ⊆ ( 𝐵 𝐶 ) )
5 4 ex ( ( 𝐴S𝐵S𝐶S ) → ( 𝐴𝐵 → ( 𝐴 𝐶 ) ⊆ ( 𝐵 𝐶 ) ) )
6 1 2 3 5 mp3an ( 𝐴𝐵 → ( 𝐴 𝐶 ) ⊆ ( 𝐵 𝐶 ) )