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

Theorem ordtr1 6222
 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 6193 . 2 (Ord 𝐶 → Tr 𝐶)
2 trel 5166 . 2 (Tr 𝐶 → ((𝐴𝐵𝐵𝐶) → 𝐴𝐶))
31, 2syl 17 1 (Ord 𝐶 → ((𝐴𝐵𝐵𝐶) → 𝐴𝐶))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 399   ∈ wcel 2115  Tr wtr 5159  Ord word 6178 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-ext 2796 This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2071  df-clab 2803  df-cleq 2817  df-clel 2896  df-v 3482  df-in 3926  df-ss 3936  df-uni 4826  df-tr 5160  df-ord 6182 This theorem is referenced by:  ontr1  6225  dfsmo2  7976  smores2  7983  smoel  7989  smogt  7996  ordiso2  8972  r1ordg  9200  r1pwss  9206  r1val1  9208  rankr1ai  9220  rankval3b  9248  rankonidlem  9250  onssr1  9253  cofsmo  9685  fpwwe2lem9  10054  bnj1098  32082  bnj594  32211  nosepssdm  33217
 Copyright terms: Public domain W3C validator