Theorem sotri 4980

Description: A strict order relation is a transitive relation. (Contributed by NM, 10-Feb-1996.) (Revised by Mario Carneiro, 10-May-2013.)

Hypotheses

Ref	Expression
soi.1	|- R Or S
soi.2	|- R C_ ( S X. S )

Assertion

Ref	Expression
sotri	|- ( ( A R B /\ B R C ) -> A R C )

Proof of Theorem sotri

Step	Hyp	Ref	Expression
1		soi.2	. . . . 5 |- R C_ ( S X. S )
2	1	brel 4637	. . . 4 |- ( A R B -> ( A e. S /\ B e. S ) )
3	2	simpld 111	. . 3 |- ( A R B -> A e. S )
4	1	brel 4637	. . 3 |- ( B R C -> ( B e. S /\ C e. S ) )
5	3, 4	anim12i 336	. 2 |- ( ( A R B /\ B R C ) -> ( A e. S /\ ( B e. S /\ C e. S ) ) )
6		soi.1	. . . 4 |- R Or S
7		sotr 4278	. . . 4 |- ( ( R Or S /\ ( A e. S /\ B e. S /\ C e. S ) ) -> ( ( A R B /\ B R C ) -> A R C ) )
8	6, 7	mpan 421	. . 3 |- ( ( A e. S /\ B e. S /\ C e. S ) -> ( ( A R B /\ B R C ) -> A R C ) )
9	8	3expb 1186	. 2 |- ( ( A e. S /\ ( B e. S /\ C e. S ) ) -> ( ( A R B /\ B R C ) -> A R C ) )
10	5, 9	mpcom 36	1 |- ( ( A R B /\ B R C ) -> A R C )

Syntax hints:   -> wi 4   /\ wa 103   /\ w3a 963   e. wcel 2128   C_ wss 3102   class class class wbr 3965   Or wor 4255   X. cxp 4583

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 604  ax-in2 605  ax-io 699  ax-5 1427  ax-7 1428  ax-gen 1429  ax-ie1 1473  ax-ie2 1474  ax-8 1484  ax-10 1485  ax-11 1486  ax-i12 1487  ax-bndl 1489  ax-4 1490  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-14 2131  ax-ext 2139  ax-sep 4082  ax-pow 4135  ax-pr 4169

This theorem depends on definitions:  df-bi 116  df-3an 965  df-tru 1338  df-nf 1441  df-sb 1743  df-clab 2144  df-cleq 2150  df-clel 2153  df-nfc 2288  df-ral 2440  df-rex 2441  df-v 2714  df-un 3106  df-in 3108  df-ss 3115  df-pw 3545  df-sn 3566  df-pr 3567  df-op 3569  df-br 3966  df-opab 4026  df-po 4256  df-iso 4257  df-xp 4591

This theorem is referenced by:  son2lpi  4981  ltsonq  7312  lt2addnq  7318  lt2mulnq  7319  ltbtwnnqq  7329  prarloclemarch2  7333  genplt2i  7424  addlocprlemgt  7448  nqprloc  7459  prmuloclemcalc  7479  ltsopr  7510  ltexprlemopl  7515  ltexprlemopu  7517  ltexprlemru  7526  prplnqu  7534  recexprlemlol  7540  recexprlemupu  7542  recexprlemdisj  7544  recexprlemss1l  7549  recexprlemss1u  7550  cauappcvgprlemopl  7560  cauappcvgprlemlol  7561  cauappcvgprlemupu  7563  cauappcvgprlemladdfu  7568  caucvgprlemk  7579  caucvgprlemnkj  7580  caucvgprlemnbj  7581  caucvgprlemm  7582  caucvgprlemopl  7583  caucvgprlemlol  7584  caucvgprlemupu  7586  caucvgprlemloc  7589  caucvgprlemladdfu  7591  caucvgprprlemk  7597  caucvgprprlemloccalc  7598  caucvgprprlemnkltj  7603  caucvgprprlemnkeqj  7604  caucvgprprlemnjltk  7605  caucvgprprlemnbj  7607  caucvgprprlemml  7608  caucvgprprlemopl  7611  caucvgprprlemlol  7612  caucvgprprlemupu  7614  lttrsr  7676  addgt0sr  7689  archsr  7696  caucvgsrlemcl  7703  caucvgsrlemfv  7705  suplocsrlemb  7720  suplocsrlempr  7721  suplocsrlem  7722  axpre-lttrn  7798