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

Theorem ordtr1 6005
 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 5976 . 2 (Ord 𝐶 → Tr 𝐶)
2 trel 4981 . 2 (Tr 𝐶 → ((𝐴𝐵𝐵𝐶) → 𝐴𝐶))
31, 2syl 17 1 (Ord 𝐶 → ((𝐴𝐵𝐵𝐶) → 𝐴𝐶))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 386   ∈ wcel 2166  Tr wtr 4974  Ord word 5961 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1896  ax-4 1910  ax-5 2011  ax-6 2077  ax-7 2114  ax-9 2175  ax-10 2194  ax-11 2209  ax-12 2222  ax-ext 2802 This theorem depends on definitions:  df-bi 199  df-an 387  df-or 881  df-tru 1662  df-ex 1881  df-nf 1885  df-sb 2070  df-clab 2811  df-cleq 2817  df-clel 2820  df-nfc 2957  df-v 3415  df-in 3804  df-ss 3811  df-uni 4658  df-tr 4975  df-ord 5965 This theorem is referenced by:  ontr1  6008  dfsmo2  7709  smores2  7716  smoel  7722  smogt  7729  ordiso2  8688  r1ordg  8917  r1pwss  8923  r1val1  8925  rankr1ai  8937  rankval3b  8965  rankonidlem  8967  onssr1  8970  cofsmo  9405  fpwwe2lem9  9774  bnj1098  31399  bnj594  31527  nosepssdm  32374
 Copyright terms: Public domain W3C validator