Metamath Proof Explorer


Theorem domentr

Description: Transitivity of dominance and equinumerosity. (Contributed by NM, 7-Jun-1998)

Ref Expression
Assertion domentr
|- ( ( A ~<_ B /\ B ~~ C ) -> A ~<_ C )

Proof

Step Hyp Ref Expression
1 endom
 |-  ( B ~~ C -> B ~<_ C )
2 domtr
 |-  ( ( A ~<_ B /\ B ~<_ C ) -> A ~<_ C )
3 1 2 sylan2
 |-  ( ( A ~<_ B /\ B ~~ C ) -> A ~<_ C )