MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ordtr1 Structured version   Visualization version   GIF version

Theorem ordtr1 6227
Description: Transitive law for ordinal classes. (Contributed by NM, 12-Dec-2004.)
Assertion
Ref Expression
ordtr1 (Ord 𝐶 → ((𝐴𝐵𝐵𝐶) → 𝐴𝐶))

Proof of Theorem ordtr1
StepHypRef Expression
1 ordtr 6198 . 2 (Ord 𝐶 → Tr 𝐶)
2 trel 5170 . 2 (Tr 𝐶 → ((𝐴𝐵𝐵𝐶) → 𝐴𝐶))
31, 2syl 17 1 (Ord 𝐶 → ((𝐴𝐵𝐵𝐶) → 𝐴𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  wcel 2105  Tr wtr 5163  Ord word 6183
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-v 3494  df-in 3940  df-ss 3949  df-uni 4831  df-tr 5164  df-ord 6187
This theorem is referenced by:  ontr1  6230  dfsmo2  7973  smores2  7980  smoel  7986  smogt  7993  ordiso2  8967  r1ordg  9195  r1pwss  9201  r1val1  9203  rankr1ai  9215  rankval3b  9243  rankonidlem  9245  onssr1  9248  cofsmo  9679  fpwwe2lem9  10048  bnj1098  31954  bnj594  32083  nosepssdm  33087
  Copyright terms: Public domain W3C validator