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 )