ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  sotri Unicode version

Theorem sotri 5019
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
StepHypRef Expression
1 soi.2 . . . . 5  |-  R  C_  ( S  X.  S
)
21brel 4674 . . . 4  |-  ( A R B  ->  ( A  e.  S  /\  B  e.  S )
)
32simpld 112 . . 3  |-  ( A R B  ->  A  e.  S )
41brel 4674 . . 3  |-  ( B R C  ->  ( B  e.  S  /\  C  e.  S )
)
53, 4anim12i 338 . 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 4314 . . . 4  |-  ( ( R  Or  S  /\  ( A  e.  S  /\  B  e.  S  /\  C  e.  S
) )  ->  (
( A R B  /\  B R C )  ->  A R C ) )
86, 7mpan 424 . . 3  |-  ( ( A  e.  S  /\  B  e.  S  /\  C  e.  S )  ->  ( ( A R B  /\  B R C )  ->  A R C ) )
983expb 1204 . 2  |-  ( ( A  e.  S  /\  ( B  e.  S  /\  C  e.  S
) )  ->  (
( A R B  /\  B R C )  ->  A R C ) )
105, 9mpcom 36 1  |-  ( ( A R B  /\  B R C )  ->  A R C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 104    /\ w3a 978    e. wcel 2148    C_ wss 3129   class class class wbr 4000    Or wor 4291    X. cxp 4620
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 614  ax-in2 615  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-14 2151  ax-ext 2159  ax-sep 4118  ax-pow 4171  ax-pr 4205
This theorem depends on definitions:  df-bi 117  df-3an 980  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ral 2460  df-rex 2461  df-v 2739  df-un 3133  df-in 3135  df-ss 3142  df-pw 3576  df-sn 3597  df-pr 3598  df-op 3600  df-br 4001  df-opab 4062  df-po 4292  df-iso 4293  df-xp 4628
This theorem is referenced by:  son2lpi  5020  ltsonq  7375  lt2addnq  7381  lt2mulnq  7382  ltbtwnnqq  7392  prarloclemarch2  7396  genplt2i  7487  addlocprlemgt  7511  nqprloc  7522  prmuloclemcalc  7542  ltsopr  7573  ltexprlemopl  7578  ltexprlemopu  7580  ltexprlemru  7589  prplnqu  7597  recexprlemlol  7603  recexprlemupu  7605  recexprlemdisj  7607  recexprlemss1l  7612  recexprlemss1u  7613  cauappcvgprlemopl  7623  cauappcvgprlemlol  7624  cauappcvgprlemupu  7626  cauappcvgprlemladdfu  7631  caucvgprlemk  7642  caucvgprlemnkj  7643  caucvgprlemnbj  7644  caucvgprlemm  7645  caucvgprlemopl  7646  caucvgprlemlol  7647  caucvgprlemupu  7649  caucvgprlemloc  7652  caucvgprlemladdfu  7654  caucvgprprlemk  7660  caucvgprprlemloccalc  7661  caucvgprprlemnkltj  7666  caucvgprprlemnkeqj  7667  caucvgprprlemnjltk  7668  caucvgprprlemnbj  7670  caucvgprprlemml  7671  caucvgprprlemopl  7674  caucvgprprlemlol  7675  caucvgprprlemupu  7677  lttrsr  7739  addgt0sr  7752  archsr  7759  caucvgsrlemcl  7766  caucvgsrlemfv  7768  suplocsrlemb  7783  suplocsrlempr  7784  suplocsrlem  7785  axpre-lttrn  7861
  Copyright terms: Public domain W3C validator