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

Theorem ordtr1 6427
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 6398 . 2 (Ord 𝐶 → Tr 𝐶)
2 trel 5268 . 2 (Tr 𝐶 → ((𝐴𝐵𝐵𝐶) → 𝐴𝐶))
31, 2syl 17 1 (Ord 𝐶 → ((𝐴𝐵𝐵𝐶) → 𝐴𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395  wcel 2108  Tr wtr 5259  Ord word 6383
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708
This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3482  df-ss 3968  df-uni 4908  df-tr 5260  df-ord 6387
This theorem is referenced by:  ontr1  6430  dfsmo2  8387  smores2  8394  smoel  8400  smogt  8407  ordiso2  9555  r1ordg  9818  r1pwss  9824  r1val1  9826  rankr1ai  9838  rankval3b  9866  rankonidlem  9868  onssr1  9871  cofsmo  10309  fpwwe2lem8  10678  nosepssdm  27731  bnj1098  34797  bnj594  34926
  Copyright terms: Public domain W3C validator