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 )