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 )

Proof

Step Hyp Ref Expression
1 ener
 |-  ~~ Er _V
2 1 a1i
 |-  ( T. -> ~~ Er _V )
3 2 ertr
 |-  ( T. -> ( ( A ~~ B /\ B ~~ C ) -> A ~~ C ) )
4 3 mptru
 |-  ( ( A ~~ B /\ B ~~ C ) -> A ~~ C )