Metamath Proof Explorer

Theorem domentr

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

Ref Expression
Assertion domentr A B B C A C


Step Hyp Ref Expression
1 endom B C B C
2 domtr A B B C A C
3 1 2 sylan2 A B B C A C