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

Theorem ordtr1 6309
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 6280 . 2 (Ord 𝐶 → Tr 𝐶)
2 trel 5198 . 2 (Tr 𝐶 → ((𝐴𝐵𝐵𝐶) → 𝐴𝐶))
31, 2syl 17 1 (Ord 𝐶 → ((𝐴𝐵𝐵𝐶) → 𝐴𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  wcel 2106  Tr wtr 5191  Ord word 6265
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709
This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-v 3434  df-in 3894  df-ss 3904  df-uni 4840  df-tr 5192  df-ord 6269
This theorem is referenced by:  ontr1  6312  dfsmo2  8178  smores2  8185  smoel  8191  smogt  8198  ordiso2  9274  r1ordg  9536  r1pwss  9542  r1val1  9544  rankr1ai  9556  rankval3b  9584  rankonidlem  9586  onssr1  9589  cofsmo  10025  fpwwe2lem8  10394  bnj1098  32763  bnj594  32892  nosepssdm  33889
  Copyright terms: Public domain W3C validator