Description: Transitivity of dominance and equinumerosity. (Contributed by NM, 7-Jun-1998)
Ref | Expression | ||
---|---|---|---|
Assertion | domentr | |- ( ( A ~<_ B /\ B ~~ C ) -> A ~<_ C ) |
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 ) |