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

Theorem sotri 4782
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 4448 . . . 4 (𝐴𝑅𝐵 → (𝐴𝑆𝐵𝑆))
32simpld 110 . . 3 (𝐴𝑅𝐵𝐴𝑆)
41brel 4448 . . 3 (𝐵𝑅𝐶 → (𝐵𝑆𝐶𝑆))
53, 4anim12i 331 . 2 ((𝐴𝑅𝐵𝐵𝑅𝐶) → (𝐴𝑆 ∧ (𝐵𝑆𝐶𝑆)))
6 soi.1 . . . 4 𝑅 Or 𝑆
7 sotr 4109 . . . 4 ((𝑅 Or 𝑆 ∧ (𝐴𝑆𝐵𝑆𝐶𝑆)) → ((𝐴𝑅𝐵𝐵𝑅𝐶) → 𝐴𝑅𝐶))
86, 7mpan 415 . . 3 ((𝐴𝑆𝐵𝑆𝐶𝑆) → ((𝐴𝑅𝐵𝐵𝑅𝐶) → 𝐴𝑅𝐶))
983expb 1140 . 2 ((𝐴𝑆 ∧ (𝐵𝑆𝐶𝑆)) → ((𝐴𝑅𝐵𝐵𝑅𝐶) → 𝐴𝑅𝐶))
105, 9mpcom 36 1 ((𝐴𝑅𝐵𝐵𝑅𝐶) → 𝐴𝑅𝐶)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 102  w3a 920  wcel 1434  wss 2984   class class class wbr 3811   Or wor 4086   × cxp 4399
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 577  ax-in2 578  ax-io 663  ax-5 1377  ax-7 1378  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-8 1436  ax-10 1437  ax-11 1438  ax-i12 1439  ax-bndl 1440  ax-4 1441  ax-14 1446  ax-17 1460  ax-i9 1464  ax-ial 1468  ax-i5r 1469  ax-ext 2065  ax-sep 3922  ax-pow 3974  ax-pr 4000
This theorem depends on definitions:  df-bi 115  df-3an 922  df-tru 1288  df-nf 1391  df-sb 1688  df-clab 2070  df-cleq 2076  df-clel 2079  df-nfc 2212  df-ral 2358  df-rex 2359  df-v 2614  df-un 2988  df-in 2990  df-ss 2997  df-pw 3408  df-sn 3428  df-pr 3429  df-op 3431  df-br 3812  df-opab 3866  df-po 4087  df-iso 4088  df-xp 4407
This theorem is referenced by:  son2lpi  4783  ltsonq  6860  lt2addnq  6866  lt2mulnq  6867  ltbtwnnqq  6877  prarloclemarch2  6881  genplt2i  6972  addlocprlemgt  6996  nqprloc  7007  prmuloclemcalc  7027  ltsopr  7058  ltexprlemopl  7063  ltexprlemopu  7065  ltexprlemru  7074  prplnqu  7082  recexprlemlol  7088  recexprlemupu  7090  recexprlemdisj  7092  recexprlemss1l  7097  recexprlemss1u  7098  cauappcvgprlemopl  7108  cauappcvgprlemlol  7109  cauappcvgprlemupu  7111  cauappcvgprlemladdfu  7116  caucvgprlemk  7127  caucvgprlemnkj  7128  caucvgprlemnbj  7129  caucvgprlemm  7130  caucvgprlemopl  7131  caucvgprlemlol  7132  caucvgprlemupu  7134  caucvgprlemloc  7137  caucvgprlemladdfu  7139  caucvgprprlemk  7145  caucvgprprlemloccalc  7146  caucvgprprlemnkltj  7151  caucvgprprlemnkeqj  7152  caucvgprprlemnjltk  7153  caucvgprprlemnbj  7155  caucvgprprlemml  7156  caucvgprprlemopl  7159  caucvgprprlemlol  7160  caucvgprprlemupu  7162  lttrsr  7211  addgt0sr  7224  archsr  7230  caucvgsrlemcl  7237  caucvgsrlemfv  7239  axpre-lttrn  7322
  Copyright terms: Public domain W3C validator