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 )