Theorem sdomdom

Description: Strict dominance implies dominance. (Contributed by NM, 10-Jun-1998)

	Ref	Expression
Assertion	sdomdom	⊢ ( 𝐴 ≺ 𝐵 → 𝐴 ≼ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		brsdom	⊢ ( 𝐴 ≺ 𝐵 ↔ ( 𝐴 ≼ 𝐵 ∧ ¬ 𝐴 ≈ 𝐵 ) )
2	1	simplbi	⊢ ( 𝐴 ≺ 𝐵 → 𝐴 ≼ 𝐵 )