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

Theorem ordtr1 4873
Description: Transitive law for ordinal classes. (Contributed by NM, 12-Dec-2004.)
Assertion
Ref Expression
ordtr1  |-  ( Ord 
C  ->  ( ( A  e.  B  /\  B  e.  C )  ->  A  e.  C ) )

Proof of Theorem ordtr1
StepHypRef Expression
1 ordtr 4844 . 2  |-  ( Ord 
C  ->  Tr  C
)
2 trel 4503 . 2  |-  ( Tr  C  ->  ( ( A  e.  B  /\  B  e.  C )  ->  A  e.  C ) )
31, 2syl 16 1  |-  ( Ord 
C  ->  ( ( A  e.  B  /\  B  e.  C )  ->  A  e.  C ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    e. wcel 1758   Tr wtr 4496   Ord word 4829
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-v 3080  df-in 3446  df-ss 3453  df-uni 4203  df-tr 4497  df-ord 4833
This theorem is referenced by:  ontr1  4876  dfsmo2  6921  smores2  6928  smoel  6934  smogt  6941  ordiso2  7843  r1ordg  8099  r1pwss  8105  r1val1  8107  rankr1ai  8119  rankval3b  8147  rankonidlem  8149  onssr1  8152  cofsmo  8552  fpwwe2lem9  8919  bnj1098  32129  bnj594  32257
  Copyright terms: Public domain W3C validator