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 4122 | . 2 | |
2 | 1 | simplbi 268 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wral 2348 wtr 3875 word 4117 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 104 |
This theorem depends on definitions: df-bi 115 df-iord 4121 |
This theorem is referenced by: ordelss 4134 ordin 4140 ordtr1 4143 orduniss 4180 ontrci 4182 ordon 4230 ordsucim 4244 ordsucss 4248 onsucsssucr 4253 onintonm 4261 ordsucunielexmid 4274 ordn2lp 4288 onsucuni2 4307 nlimsucg 4309 ordpwsucss 4310 tfrexlem 5971 |
Copyright terms: Public domain | W3C validator |