Metamath Proof Explorer

Theorem sdomentr

Description: Transitivity of strict dominance and equinumerosity. Exercise 11 of Suppes p. 98. (Contributed by NM, 26-Oct-2003)

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

Proof

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