Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > ordtr | Unicode version |
Description: An ordinal class is transitive. (Contributed by NM, 3-Apr-1994.) |
Ref | Expression |
---|---|
ordtr |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dford3 4259 | . 2 | |
2 | 1 | simplbi 272 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wral 2393 wtr 3996 word 4254 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 |
This theorem depends on definitions: df-bi 116 df-iord 4258 |
This theorem is referenced by: ordelss 4271 ordin 4277 ordtr1 4280 orduniss 4317 ontrci 4319 ordon 4372 ordsucim 4386 ordsucss 4390 onsucsssucr 4395 onintonm 4403 ordsucunielexmid 4416 ordn2lp 4430 onsucuni2 4449 nlimsucg 4451 ordpwsucss 4452 tfrexlem 6199 nnsucuniel 6359 ctmlemr 6961 nnnninf 6991 ctinf 11870 nnsf 13126 peano4nninf 13127 nninfalllemn 13129 |
Copyright terms: Public domain | W3C validator |