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

Theorem sotri 4904
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 4561 . . . 4 (𝐴𝑅𝐵 → (𝐴𝑆𝐵𝑆))
32simpld 111 . . 3 (𝐴𝑅𝐵𝐴𝑆)
41brel 4561 . . 3 (𝐵𝑅𝐶 → (𝐵𝑆𝐶𝑆))
53, 4anim12i 336 . 2 ((𝐴𝑅𝐵𝐵𝑅𝐶) → (𝐴𝑆 ∧ (𝐵𝑆𝐶𝑆)))
6 soi.1 . . . 4 𝑅 Or 𝑆
7 sotr 4210 . . . 4 ((𝑅 Or 𝑆 ∧ (𝐴𝑆𝐵𝑆𝐶𝑆)) → ((𝐴𝑅𝐵𝐵𝑅𝐶) → 𝐴𝑅𝐶))
86, 7mpan 420 . . 3 ((𝐴𝑆𝐵𝑆𝐶𝑆) → ((𝐴𝑅𝐵𝐵𝑅𝐶) → 𝐴𝑅𝐶))
983expb 1167 . 2 ((𝐴𝑆 ∧ (𝐵𝑆𝐶𝑆)) → ((𝐴𝑅𝐵𝐵𝑅𝐶) → 𝐴𝑅𝐶))
105, 9mpcom 36 1 ((𝐴𝑅𝐵𝐵𝑅𝐶) → 𝐴𝑅𝐶)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103  w3a 947  wcel 1465  wss 3041   class class class wbr 3899   Or wor 4187   × cxp 4507
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 588  ax-in2 589  ax-io 683  ax-5 1408  ax-7 1409  ax-gen 1410  ax-ie1 1454  ax-ie2 1455  ax-8 1467  ax-10 1468  ax-11 1469  ax-i12 1470  ax-bndl 1471  ax-4 1472  ax-14 1477  ax-17 1491  ax-i9 1495  ax-ial 1499  ax-i5r 1500  ax-ext 2099  ax-sep 4016  ax-pow 4068  ax-pr 4101
This theorem depends on definitions:  df-bi 116  df-3an 949  df-tru 1319  df-nf 1422  df-sb 1721  df-clab 2104  df-cleq 2110  df-clel 2113  df-nfc 2247  df-ral 2398  df-rex 2399  df-v 2662  df-un 3045  df-in 3047  df-ss 3054  df-pw 3482  df-sn 3503  df-pr 3504  df-op 3506  df-br 3900  df-opab 3960  df-po 4188  df-iso 4189  df-xp 4515
This theorem is referenced by:  son2lpi  4905  ltsonq  7174  lt2addnq  7180  lt2mulnq  7181  ltbtwnnqq  7191  prarloclemarch2  7195  genplt2i  7286  addlocprlemgt  7310  nqprloc  7321  prmuloclemcalc  7341  ltsopr  7372  ltexprlemopl  7377  ltexprlemopu  7379  ltexprlemru  7388  prplnqu  7396  recexprlemlol  7402  recexprlemupu  7404  recexprlemdisj  7406  recexprlemss1l  7411  recexprlemss1u  7412  cauappcvgprlemopl  7422  cauappcvgprlemlol  7423  cauappcvgprlemupu  7425  cauappcvgprlemladdfu  7430  caucvgprlemk  7441  caucvgprlemnkj  7442  caucvgprlemnbj  7443  caucvgprlemm  7444  caucvgprlemopl  7445  caucvgprlemlol  7446  caucvgprlemupu  7448  caucvgprlemloc  7451  caucvgprlemladdfu  7453  caucvgprprlemk  7459  caucvgprprlemloccalc  7460  caucvgprprlemnkltj  7465  caucvgprprlemnkeqj  7466  caucvgprprlemnjltk  7467  caucvgprprlemnbj  7469  caucvgprprlemml  7470  caucvgprprlemopl  7473  caucvgprprlemlol  7474  caucvgprprlemupu  7476  lttrsr  7538  addgt0sr  7551  archsr  7558  caucvgsrlemcl  7565  caucvgsrlemfv  7567  suplocsrlemb  7582  suplocsrlempr  7583  suplocsrlem  7584  axpre-lttrn  7660
  Copyright terms: Public domain W3C validator