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

Theorem sotri 5024
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 𝑅 Or 𝑆
soi.2 𝑅 ⊆ (𝑆 × 𝑆)
Assertion
Ref Expression
sotri ((𝐴𝑅𝐵𝐵𝑅𝐶) → 𝐴𝑅𝐶)

Proof of Theorem sotri
StepHypRef Expression
1 soi.2 . . . . 5 𝑅 ⊆ (𝑆 × 𝑆)
21brel 4678 . . . 4 (𝐴𝑅𝐵 → (𝐴𝑆𝐵𝑆))
32simpld 112 . . 3 (𝐴𝑅𝐵𝐴𝑆)
41brel 4678 . . 3 (𝐵𝑅𝐶 → (𝐵𝑆𝐶𝑆))
53, 4anim12i 338 . 2 ((𝐴𝑅𝐵𝐵𝑅𝐶) → (𝐴𝑆 ∧ (𝐵𝑆𝐶𝑆)))
6 soi.1 . . . 4 𝑅 Or 𝑆
7 sotr 4318 . . . 4 ((𝑅 Or 𝑆 ∧ (𝐴𝑆𝐵𝑆𝐶𝑆)) → ((𝐴𝑅𝐵𝐵𝑅𝐶) → 𝐴𝑅𝐶))
86, 7mpan 424 . . 3 ((𝐴𝑆𝐵𝑆𝐶𝑆) → ((𝐴𝑅𝐵𝐵𝑅𝐶) → 𝐴𝑅𝐶))
983expb 1204 . 2 ((𝐴𝑆 ∧ (𝐵𝑆𝐶𝑆)) → ((𝐴𝑅𝐵𝐵𝑅𝐶) → 𝐴𝑅𝐶))
105, 9mpcom 36 1 ((𝐴𝑅𝐵𝐵𝑅𝐶) → 𝐴𝑅𝐶)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 104  w3a 978  wcel 2148  wss 3129   class class class wbr 4003   Or wor 4295   × cxp 4624
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 4121  ax-pow 4174  ax-pr 4209
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 3577  df-sn 3598  df-pr 3599  df-op 3601  df-br 4004  df-opab 4065  df-po 4296  df-iso 4297  df-xp 4632
This theorem is referenced by:  son2lpi  5025  ltsonq  7396  lt2addnq  7402  lt2mulnq  7403  ltbtwnnqq  7413  prarloclemarch2  7417  genplt2i  7508  addlocprlemgt  7532  nqprloc  7543  prmuloclemcalc  7563  ltsopr  7594  ltexprlemopl  7599  ltexprlemopu  7601  ltexprlemru  7610  prplnqu  7618  recexprlemlol  7624  recexprlemupu  7626  recexprlemdisj  7628  recexprlemss1l  7633  recexprlemss1u  7634  cauappcvgprlemopl  7644  cauappcvgprlemlol  7645  cauappcvgprlemupu  7647  cauappcvgprlemladdfu  7652  caucvgprlemk  7663  caucvgprlemnkj  7664  caucvgprlemnbj  7665  caucvgprlemm  7666  caucvgprlemopl  7667  caucvgprlemlol  7668  caucvgprlemupu  7670  caucvgprlemloc  7673  caucvgprlemladdfu  7675  caucvgprprlemk  7681  caucvgprprlemloccalc  7682  caucvgprprlemnkltj  7687  caucvgprprlemnkeqj  7688  caucvgprprlemnjltk  7689  caucvgprprlemnbj  7691  caucvgprprlemml  7692  caucvgprprlemopl  7695  caucvgprprlemlol  7696  caucvgprprlemupu  7698  lttrsr  7760  addgt0sr  7773  archsr  7780  caucvgsrlemcl  7787  caucvgsrlemfv  7789  suplocsrlemb  7804  suplocsrlempr  7805  suplocsrlem  7806  axpre-lttrn  7882
  Copyright terms: Public domain W3C validator