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

Step	Hyp	Ref	Expression
1		ordtr 4844	. 2 |- ( Ord C -> Tr C )
2		trel 4503	. 2 |- ( Tr C -> ( ( A e. B /\ B e. C ) -> A e. C ) )
3	1, 2	syl 16	1 |- ( Ord C -> ( ( A e. B /\ B e. C ) -> A e. C ) )

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