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

Metamath Proof Explorer

Theorem domentr

Description: Transitivity of dominance and equinumerosity. (Contributed by NM, 7-Jun-1998)

		Ref	Expression
	Assertion	domentr	$⊢ (A ≼ B \land B \approx C) \to A ≼ C$

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