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

Theorem sotri 4720
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 4392 . . . 4  |-  ( A R B  ->  ( A  e.  S  /\  B  e.  S )
)
32simpld 105 . . 3  |-  ( A R B  ->  A  e.  S )
41brel 4392 . . 3  |-  ( B R C  ->  ( B  e.  S  /\  C  e.  S )
)
53, 4anim12i 321 . 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 4055 . . . 4  |-  ( ( R  Or  S  /\  ( A  e.  S  /\  B  e.  S  /\  C  e.  S
) )  ->  (
( A R B  /\  B R C )  ->  A R C ) )
86, 7mpan 400 . . 3  |-  ( ( A  e.  S  /\  B  e.  S  /\  C  e.  S )  ->  ( ( A R B  /\  B R C )  ->  A R C ) )
983expb 1105 . 2  |-  ( ( A  e.  S  /\  ( B  e.  S  /\  C  e.  S
) )  ->  (
( A R B  /\  B R C )  ->  A R C ) )
105, 9mpcom 32 1  |-  ( ( A R B  /\  B R C )  ->  A R C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 97    /\ w3a 885    e. wcel 1393    C_ wss 2917   class class class wbr 3764    Or wor 4032    X. cxp 4343
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-in1 544  ax-in2 545  ax-io 630  ax-5 1336  ax-7 1337  ax-gen 1338  ax-ie1 1382  ax-ie2 1383  ax-8 1395  ax-10 1396  ax-11 1397  ax-i12 1398  ax-bndl 1399  ax-4 1400  ax-14 1405  ax-17 1419  ax-i9 1423  ax-ial 1427  ax-i5r 1428  ax-ext 2022  ax-sep 3875  ax-pow 3927  ax-pr 3944
This theorem depends on definitions:  df-bi 110  df-3an 887  df-tru 1246  df-nf 1350  df-sb 1646  df-clab 2027  df-cleq 2033  df-clel 2036  df-nfc 2167  df-ral 2311  df-rex 2312  df-v 2559  df-un 2922  df-in 2924  df-ss 2931  df-pw 3361  df-sn 3381  df-pr 3382  df-op 3384  df-br 3765  df-opab 3819  df-po 4033  df-iso 4034  df-xp 4351
This theorem is referenced by:  son2lpi  4721  ltsonq  6496  lt2addnq  6502  lt2mulnq  6503  ltbtwnnqq  6513  prarloclemarch2  6517  genplt2i  6608  addlocprlemgt  6632  nqprloc  6643  prmuloclemcalc  6663  ltsopr  6694  ltexprlemopl  6699  ltexprlemopu  6701  ltexprlemru  6710  prplnqu  6718  recexprlemlol  6724  recexprlemupu  6726  recexprlemdisj  6728  recexprlemss1l  6733  recexprlemss1u  6734  cauappcvgprlemopl  6744  cauappcvgprlemlol  6745  cauappcvgprlemupu  6747  cauappcvgprlemladdfu  6752  caucvgprlemk  6763  caucvgprlemnkj  6764  caucvgprlemnbj  6765  caucvgprlemm  6766  caucvgprlemopl  6767  caucvgprlemlol  6768  caucvgprlemupu  6770  caucvgprlemloc  6773  caucvgprlemladdfu  6775  caucvgprprlemk  6781  caucvgprprlemloccalc  6782  caucvgprprlemnkltj  6787  caucvgprprlemnkeqj  6788  caucvgprprlemnjltk  6789  caucvgprprlemnbj  6791  caucvgprprlemml  6792  caucvgprprlemopl  6795  caucvgprprlemlol  6796  caucvgprprlemupu  6798  lttrsr  6847  addgt0sr  6860  archsr  6866  caucvgsrlemcl  6873  caucvgsrlemfv  6875  axpre-lttrn  6958
  Copyright terms: Public domain W3C validator