Theorem ordtr 6280

Description: An ordinal class is transitive. (Contributed by NM, 3-Apr-1994.)

Assertion

Ref	Expression
ordtr	⊢ (Ord 𝐴 → Tr 𝐴)

Proof of Theorem ordtr

Step	Hyp	Ref	Expression
1		df-ord 6269	. 2 ⊢ (Ord 𝐴 ↔ (Tr 𝐴 ∧ E We 𝐴))
2	1	simplbi 498	1 ⊢ (Ord 𝐴 → Tr 𝐴)

Syntax hints:   → wi 4  Tr wtr 5191   E cep 5494   We wwe 5543  Ord word 6265

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 206  df-an 397  df-ord 6269

This theorem is referenced by:  ordelss  6282  ordn2lp  6286  ordelord  6288  tz7.7  6292  ordelssne  6293  ordin  6296  ordtr1  6309  orduniss  6360  ontrci  6372  ordunisuc  7679  onuninsuci  7687  limsuc  7696  trom  7721  omsindsOLD  7734  dfrecs3  8203  dfrecs3OLD  8204  tz7.44-2  8238  cantnflt  9430  cantnfp1lem3  9438  cantnflem1b  9444  cantnflem1  9447  cnfcom  9458  axdc3lem2  10207  inar1  10531  efgmnvl  19320  bnj967  32925  dford5  33671  dford3  40850  limsuc2  40866  nlimsuc  41048  ordelordALT  42157  onfrALTlem2  42166  ordelordALTVD  42487  onfrALTlem2VD  42509  iunord  46382