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

Theorem sotri 4827
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 4490 . . . 4  |-  ( A R B  ->  ( A  e.  S  /\  B  e.  S )
)
32simpld 110 . . 3  |-  ( A R B  ->  A  e.  S )
41brel 4490 . . 3  |-  ( B R C  ->  ( B  e.  S  /\  C  e.  S )
)
53, 4anim12i 331 . 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 4145 . . . 4  |-  ( ( R  Or  S  /\  ( A  e.  S  /\  B  e.  S  /\  C  e.  S
) )  ->  (
( A R B  /\  B R C )  ->  A R C ) )
86, 7mpan 415 . . 3  |-  ( ( A  e.  S  /\  B  e.  S  /\  C  e.  S )  ->  ( ( A R B  /\  B R C )  ->  A R C ) )
983expb 1144 . 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 102    /\ w3a 924    e. wcel 1438    C_ wss 2999   class class class wbr 3845    Or wor 4122    X. cxp 4436
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-in1 579  ax-in2 580  ax-io 665  ax-5 1381  ax-7 1382  ax-gen 1383  ax-ie1 1427  ax-ie2 1428  ax-8 1440  ax-10 1441  ax-11 1442  ax-i12 1443  ax-bndl 1444  ax-4 1445  ax-14 1450  ax-17 1464  ax-i9 1468  ax-ial 1472  ax-i5r 1473  ax-ext 2070  ax-sep 3957  ax-pow 4009  ax-pr 4036
This theorem depends on definitions:  df-bi 115  df-3an 926  df-tru 1292  df-nf 1395  df-sb 1693  df-clab 2075  df-cleq 2081  df-clel 2084  df-nfc 2217  df-ral 2364  df-rex 2365  df-v 2621  df-un 3003  df-in 3005  df-ss 3012  df-pw 3431  df-sn 3452  df-pr 3453  df-op 3455  df-br 3846  df-opab 3900  df-po 4123  df-iso 4124  df-xp 4444
This theorem is referenced by:  son2lpi  4828  ltsonq  6957  lt2addnq  6963  lt2mulnq  6964  ltbtwnnqq  6974  prarloclemarch2  6978  genplt2i  7069  addlocprlemgt  7093  nqprloc  7104  prmuloclemcalc  7124  ltsopr  7155  ltexprlemopl  7160  ltexprlemopu  7162  ltexprlemru  7171  prplnqu  7179  recexprlemlol  7185  recexprlemupu  7187  recexprlemdisj  7189  recexprlemss1l  7194  recexprlemss1u  7195  cauappcvgprlemopl  7205  cauappcvgprlemlol  7206  cauappcvgprlemupu  7208  cauappcvgprlemladdfu  7213  caucvgprlemk  7224  caucvgprlemnkj  7225  caucvgprlemnbj  7226  caucvgprlemm  7227  caucvgprlemopl  7228  caucvgprlemlol  7229  caucvgprlemupu  7231  caucvgprlemloc  7234  caucvgprlemladdfu  7236  caucvgprprlemk  7242  caucvgprprlemloccalc  7243  caucvgprprlemnkltj  7248  caucvgprprlemnkeqj  7249  caucvgprprlemnjltk  7250  caucvgprprlemnbj  7252  caucvgprprlemml  7253  caucvgprprlemopl  7256  caucvgprprlemlol  7257  caucvgprprlemupu  7259  lttrsr  7308  addgt0sr  7321  archsr  7327  caucvgsrlemcl  7334  caucvgsrlemfv  7336  axpre-lttrn  7419
  Copyright terms: Public domain W3C validator