Metamath Proof Explorer

Theorem enen1

Description: Equality-like theorem for equinumerosity. (Contributed by NM, 18-Dec-2003)

Ref Expression
Assertion enen1 
|- ( A ~~ B -> ( A ~~ C <-> B ~~ C ) )

Proof

Step Hyp Ref Expression
1 ensym 
 |-  ( A ~~ B -> B ~~ A )
2 entr 
 |-  ( ( B ~~ A /\ A ~~ C ) -> B ~~ C )
3 1 2 sylan 
 |-  ( ( A ~~ B /\ A ~~ C ) -> B ~~ C )
4 entr 
 |-  ( ( A ~~ B /\ B ~~ C ) -> A ~~ C )
5 3 4 impbida 
 |-  ( A ~~ B -> ( A ~~ C <-> B ~~ C ) )