Metamath Proof Explorer

Theorem entr

Description: Transitivity of equinumerosity. Theorem 3 of Suppes p. 92. (Contributed by NM, 9-Jun-1998)

Ref Expression
Assertion entr A B B C A C


Step Hyp Ref Expression
1 ener Er V
2 1 a1i Er V
3 2 ertr A B B C A C
4 3 mptru A B B C A C