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

Theorem sotri 5006
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 4663 . . . 4 (𝐴𝑅𝐵 → (𝐴𝑆𝐵𝑆))
32simpld 111 . . 3 (𝐴𝑅𝐵𝐴𝑆)
41brel 4663 . . 3 (𝐵𝑅𝐶 → (𝐵𝑆𝐶𝑆))
53, 4anim12i 336 . 2 ((𝐴𝑅𝐵𝐵𝑅𝐶) → (𝐴𝑆 ∧ (𝐵𝑆𝐶𝑆)))
6 soi.1 . . . 4 𝑅 Or 𝑆
7 sotr 4303 . . . 4 ((𝑅 Or 𝑆 ∧ (𝐴𝑆𝐵𝑆𝐶𝑆)) → ((𝐴𝑅𝐵𝐵𝑅𝐶) → 𝐴𝑅𝐶))
86, 7mpan 422 . . 3 ((𝐴𝑆𝐵𝑆𝐶𝑆) → ((𝐴𝑅𝐵𝐵𝑅𝐶) → 𝐴𝑅𝐶))
983expb 1199 . 2 ((𝐴𝑆 ∧ (𝐵𝑆𝐶𝑆)) → ((𝐴𝑅𝐵𝐵𝑅𝐶) → 𝐴𝑅𝐶))
105, 9mpcom 36 1 ((𝐴𝑅𝐵𝐵𝑅𝐶) → 𝐴𝑅𝐶)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103  w3a 973  wcel 2141  wss 3121   class class class wbr 3989   Or wor 4280   × cxp 4609
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 609  ax-in2 610  ax-io 704  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-10 1498  ax-11 1499  ax-i12 1500  ax-bndl 1502  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-14 2144  ax-ext 2152  ax-sep 4107  ax-pow 4160  ax-pr 4194
This theorem depends on definitions:  df-bi 116  df-3an 975  df-tru 1351  df-nf 1454  df-sb 1756  df-clab 2157  df-cleq 2163  df-clel 2166  df-nfc 2301  df-ral 2453  df-rex 2454  df-v 2732  df-un 3125  df-in 3127  df-ss 3134  df-pw 3568  df-sn 3589  df-pr 3590  df-op 3592  df-br 3990  df-opab 4051  df-po 4281  df-iso 4282  df-xp 4617
This theorem is referenced by:  son2lpi  5007  ltsonq  7360  lt2addnq  7366  lt2mulnq  7367  ltbtwnnqq  7377  prarloclemarch2  7381  genplt2i  7472  addlocprlemgt  7496  nqprloc  7507  prmuloclemcalc  7527  ltsopr  7558  ltexprlemopl  7563  ltexprlemopu  7565  ltexprlemru  7574  prplnqu  7582  recexprlemlol  7588  recexprlemupu  7590  recexprlemdisj  7592  recexprlemss1l  7597  recexprlemss1u  7598  cauappcvgprlemopl  7608  cauappcvgprlemlol  7609  cauappcvgprlemupu  7611  cauappcvgprlemladdfu  7616  caucvgprlemk  7627  caucvgprlemnkj  7628  caucvgprlemnbj  7629  caucvgprlemm  7630  caucvgprlemopl  7631  caucvgprlemlol  7632  caucvgprlemupu  7634  caucvgprlemloc  7637  caucvgprlemladdfu  7639  caucvgprprlemk  7645  caucvgprprlemloccalc  7646  caucvgprprlemnkltj  7651  caucvgprprlemnkeqj  7652  caucvgprprlemnjltk  7653  caucvgprprlemnbj  7655  caucvgprprlemml  7656  caucvgprprlemopl  7659  caucvgprprlemlol  7660  caucvgprprlemupu  7662  lttrsr  7724  addgt0sr  7737  archsr  7744  caucvgsrlemcl  7751  caucvgsrlemfv  7753  suplocsrlemb  7768  suplocsrlempr  7769  suplocsrlem  7770  axpre-lttrn  7846
  Copyright terms: Public domain W3C validator