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

Theorem ordtr1 4757
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 4728 . 2  |-  ( Ord 
C  ->  Tr  C
)
2 trel 4387 . 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 1756   Tr wtr 4380   Ord word 4713
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-v 2969  df-in 3330  df-ss 3337  df-uni 4087  df-tr 4381  df-ord 4717
This theorem is referenced by:  ontr1  4760  dfsmo2  6800  smores2  6807  smoel  6813  smogt  6820  ordiso2  7721  r1ordg  7977  r1pwss  7983  r1val1  7985  rankr1ai  7997  rankval3b  8025  rankonidlem  8027  onssr1  8030  cofsmo  8430  fpwwe2lem9  8797  bnj1098  31664  bnj594  31792
  Copyright terms: Public domain W3C validator