Theorem ordtr1 5466

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 5437	. 2 |- ( Ord C -> Tr C )
2		trel 4504	. 2 |- ( Tr C -> ( ( A e. B /\ B e. C ) -> A e. C ) )
3	1, 2	syl 17	1 |- ( Ord C -> ( ( A e. B /\ B e. C ) -> A e. C ) )

Syntax hints:   -> wi 4   /\ wa 371   e. wcel 1887   Tr wtr 4497   Ord word 5422

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-5 1758  ax-6 1805  ax-7 1851  ax-10 1915  ax-11 1920  ax-12 1933  ax-13 2091  ax-ext 2431

This theorem depends on definitions:  df-bi 189  df-an 373  df-tru 1447  df-ex 1664  df-nf 1668  df-sb 1798  df-clab 2438  df-cleq 2444  df-clel 2447  df-nfc 2581  df-v 3047  df-in 3411  df-ss 3418  df-uni 4199  df-tr 4498  df-ord 5426

This theorem is referenced by:  ontr1  5469  dfsmo2  7066  smores2  7073  smoel  7079  smogt  7086  ordiso2  8030  r1ordg  8249  r1pwss  8255  r1val1  8257  rankr1ai  8269  rankval3b  8297  rankonidlem  8299  onssr1  8302  cofsmo  8699  fpwwe2lem9  9063  bnj1098  29595  bnj594  29723