Description: Alias for axlttrn , for naming consistency with lttri . New proofs should generally use this instead of ax-pre-lttrn . (Contributed by NM, 10-Mar-2008)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | lttr | |- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( A < B /\ B < C ) -> A < C ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | axlttrn | |- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( A < B /\ B < C ) -> A < C ) ) |