Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > ordtr1 | Structured version Visualization version Unicode version |
Description: Transitive law for ordinal classes. (Contributed by NM, 12-Dec-2004.) |
Ref | Expression |
---|---|
ordtr1 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ordtr 5737 | . 2 | |
2 | trel 4759 | . 2 | |
3 | 1, 2 | syl 17 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wi 4 wa 384 wcel 1990 wtr 4752 word 5722 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 |
This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-v 3202 df-in 3581 df-ss 3588 df-uni 4437 df-tr 4753 df-ord 5726 |
This theorem is referenced by: ontr1 5771 dfsmo2 7444 smores2 7451 smoel 7457 smogt 7464 ordiso2 8420 r1ordg 8641 r1pwss 8647 r1val1 8649 rankr1ai 8661 rankval3b 8689 rankonidlem 8691 onssr1 8694 cofsmo 9091 fpwwe2lem9 9460 bnj1098 30854 bnj594 30982 nosepssdm 31836 |
Copyright terms: Public domain | W3C validator |