Metamath Proof Explorer


Theorem endomtr

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

Ref Expression
Assertion endomtr A B B C A C

Proof

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