Theorem sotri 4934

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 4591	. . . 4 |- ( A R B -> ( A e. S /\ B e. S ) )
3	2	simpld 111	. . 3 |- ( A R B -> A e. S )
4	1	brel 4591	. . 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 4240	. . . 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 420	. . 3 |- ( ( A e. S /\ B e. S /\ C e. S ) -> ( ( A R B /\ B R C ) -> A R C ) )
9	8	3expb 1182	. 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 962   e. wcel 1480   C_ wss 3071   class class class wbr 3929   Or wor 4217   X. cxp 4537

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 603  ax-in2 604  ax-io 698  ax-5 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-10 1483  ax-11 1484  ax-i12 1485  ax-bndl 1486  ax-4 1487  ax-14 1492  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2121  ax-sep 4046  ax-pow 4098  ax-pr 4131

This theorem depends on definitions:  df-bi 116  df-3an 964  df-tru 1334  df-nf 1437  df-sb 1736  df-clab 2126  df-cleq 2132  df-clel 2135  df-nfc 2270  df-ral 2421  df-rex 2422  df-v 2688  df-un 3075  df-in 3077  df-ss 3084  df-pw 3512  df-sn 3533  df-pr 3534  df-op 3536  df-br 3930  df-opab 3990  df-po 4218  df-iso 4219  df-xp 4545

This theorem is referenced by:  son2lpi  4935  ltsonq  7206  lt2addnq  7212  lt2mulnq  7213  ltbtwnnqq  7223  prarloclemarch2  7227  genplt2i  7318  addlocprlemgt  7342  nqprloc  7353  prmuloclemcalc  7373  ltsopr  7404  ltexprlemopl  7409  ltexprlemopu  7411  ltexprlemru  7420  prplnqu  7428  recexprlemlol  7434  recexprlemupu  7436  recexprlemdisj  7438  recexprlemss1l  7443  recexprlemss1u  7444  cauappcvgprlemopl  7454  cauappcvgprlemlol  7455  cauappcvgprlemupu  7457  cauappcvgprlemladdfu  7462  caucvgprlemk  7473  caucvgprlemnkj  7474  caucvgprlemnbj  7475  caucvgprlemm  7476  caucvgprlemopl  7477  caucvgprlemlol  7478  caucvgprlemupu  7480  caucvgprlemloc  7483  caucvgprlemladdfu  7485  caucvgprprlemk  7491  caucvgprprlemloccalc  7492  caucvgprprlemnkltj  7497  caucvgprprlemnkeqj  7498  caucvgprprlemnjltk  7499  caucvgprprlemnbj  7501  caucvgprprlemml  7502  caucvgprprlemopl  7505  caucvgprprlemlol  7506  caucvgprprlemupu  7508  lttrsr  7570  addgt0sr  7583  archsr  7590  caucvgsrlemcl  7597  caucvgsrlemfv  7599  suplocsrlemb  7614  suplocsrlempr  7615  suplocsrlem  7616  axpre-lttrn  7692