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

Theorem ordtr1 6407
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 6378 . 2 (Ord 𝐶 → Tr 𝐶)
2 trel 5274 . 2 (Tr 𝐶 → ((𝐴𝐵𝐵𝐶) → 𝐴𝐶))
31, 2syl 17 1 (Ord 𝐶 → ((𝐴𝐵𝐵𝐶) → 𝐴𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395  wcel 2105  Tr wtr 5265  Ord word 6363
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2702
This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1543  df-ex 1781  df-sb 2067  df-clab 2709  df-cleq 2723  df-clel 2809  df-v 3475  df-in 3955  df-ss 3965  df-uni 4909  df-tr 5266  df-ord 6367
This theorem is referenced by:  ontr1  6410  dfsmo2  8350  smores2  8357  smoel  8363  smogt  8370  ordiso2  9513  r1ordg  9776  r1pwss  9782  r1val1  9784  rankr1ai  9796  rankval3b  9824  rankonidlem  9826  onssr1  9829  cofsmo  10267  fpwwe2lem8  10636  nosepssdm  27426  bnj1098  34093  bnj594  34222
  Copyright terms: Public domain W3C validator