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

Theorem ordtr1 6429
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 6400 . 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 2106  Tr wtr 5265  Ord word 6385
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706
This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-v 3480  df-ss 3980  df-uni 4913  df-tr 5266  df-ord 6389
This theorem is referenced by:  ontr1  6432  dfsmo2  8386  smores2  8393  smoel  8399  smogt  8406  ordiso2  9553  r1ordg  9816  r1pwss  9822  r1val1  9824  rankr1ai  9836  rankval3b  9864  rankonidlem  9866  onssr1  9869  cofsmo  10307  fpwwe2lem8  10676  nosepssdm  27746  bnj1098  34776  bnj594  34905
  Copyright terms: Public domain W3C validator