This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem sdomentr

Description: Transitivity of strict dominance and equinumerosity. Exercise 11 of Suppes p. 98. (Contributed by NM, 26-Oct-2003)

		Ref	Expression
	Assertion	sdomentr	$⊢ (A ≺ B \land B \approx C) \to A ≺ C$

Step	Hyp	Ref	Expression
1		endom	$⊢ B \approx C \to B ≼ C$
2		sdomdomtr	$⊢ (A ≺ B \land B ≼ C) \to A ≺ C$
3	1 2	sylan2	$⊢ (A ≺ B \land B \approx C) \to A ≺ C$