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

Theorem ordtr1 6216
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 6187 . 2 (Ord 𝐶 → Tr 𝐶)
2 trel 5144 . 2 (Tr 𝐶 → ((𝐴𝐵𝐵𝐶) → 𝐴𝐶))
31, 2syl 17 1 (Ord 𝐶 → ((𝐴𝐵𝐵𝐶) → 𝐴𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399  wcel 2114  Tr wtr 5137  Ord word 6172
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2020  ax-8 2116  ax-9 2124  ax-ext 2711
This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1545  df-ex 1787  df-sb 2075  df-clab 2718  df-cleq 2731  df-clel 2812  df-v 3401  df-in 3851  df-ss 3861  df-uni 4798  df-tr 5138  df-ord 6176
This theorem is referenced by:  ontr1  6219  dfsmo2  8016  smores2  8023  smoel  8029  smogt  8036  ordiso2  9055  r1ordg  9283  r1pwss  9289  r1val1  9291  rankr1ai  9303  rankval3b  9331  rankonidlem  9333  onssr1  9336  cofsmo  9772  fpwwe2lem8  10141  bnj1098  32337  bnj594  32466  nosepssdm  33535
  Copyright terms: Public domain W3C validator