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

Theorem caovord2d 5722
Description: Operation ordering law with commuted arguments. (Contributed by Mario Carneiro, 30-Dec-2014.)
Hypotheses
Ref Expression
caovordg.1 ((𝜑 ∧ (𝑥𝑆𝑦𝑆𝑧𝑆)) → (𝑥𝑅𝑦 ↔ (𝑧𝐹𝑥)𝑅(𝑧𝐹𝑦)))
caovordd.2 (𝜑𝐴𝑆)
caovordd.3 (𝜑𝐵𝑆)
caovordd.4 (𝜑𝐶𝑆)
caovord2d.com ((𝜑 ∧ (𝑥𝑆𝑦𝑆)) → (𝑥𝐹𝑦) = (𝑦𝐹𝑥))
Assertion
Ref Expression
caovord2d (𝜑 → (𝐴𝑅𝐵 ↔ (𝐴𝐹𝐶)𝑅(𝐵𝐹𝐶)))
Distinct variable groups:   𝑥,𝑦,𝑧,𝐴   𝑥,𝐵,𝑦,𝑧   𝑥,𝐶,𝑦,𝑧   𝜑,𝑥,𝑦,𝑧   𝑥,𝐹,𝑦,𝑧   𝑥,𝑅,𝑦,𝑧   𝑥,𝑆,𝑦,𝑧

Proof of Theorem caovord2d
StepHypRef Expression
1 caovordg.1 . . 3 ((𝜑 ∧ (𝑥𝑆𝑦𝑆𝑧𝑆)) → (𝑥𝑅𝑦 ↔ (𝑧𝐹𝑥)𝑅(𝑧𝐹𝑦)))
2 caovordd.2 . . 3 (𝜑𝐴𝑆)
3 caovordd.3 . . 3 (𝜑𝐵𝑆)
4 caovordd.4 . . 3 (𝜑𝐶𝑆)
51, 2, 3, 4caovordd 5721 . 2 (𝜑 → (𝐴𝑅𝐵 ↔ (𝐶𝐹𝐴)𝑅(𝐶𝐹𝐵)))
6 caovord2d.com . . . 4 ((𝜑 ∧ (𝑥𝑆𝑦𝑆)) → (𝑥𝐹𝑦) = (𝑦𝐹𝑥))
76, 4, 2caovcomd 5709 . . 3 (𝜑 → (𝐶𝐹𝐴) = (𝐴𝐹𝐶))
86, 4, 3caovcomd 5709 . . 3 (𝜑 → (𝐶𝐹𝐵) = (𝐵𝐹𝐶))
97, 8breq12d 3818 . 2 (𝜑 → ((𝐶𝐹𝐴)𝑅(𝐶𝐹𝐵) ↔ (𝐴𝐹𝐶)𝑅(𝐵𝐹𝐶)))
105, 9bitrd 186 1 (𝜑 → (𝐴𝑅𝐵 ↔ (𝐴𝐹𝐶)𝑅(𝐵𝐹𝐶)))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 102  wb 103  w3a 920   = wceq 1285  wcel 1434   class class class wbr 3805  (class class class)co 5564
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-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-17 1460  ax-i9 1464  ax-ial 1468  ax-i5r 1469  ax-ext 2065
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 2612  df-un 2986  df-sn 3422  df-pr 3423  df-op 3425  df-uni 3622  df-br 3806  df-iota 4917  df-fv 4960  df-ov 5567
This theorem is referenced by:  caovord3d  5723  genplt2i  6832  addnqprllem  6849  addnqprulem  6850  mulnqprl  6890  mulnqpru  6891  distrlem4prl  6906  distrlem4pru  6907  1idprl  6912  1idpru  6913  ltexprlemdisj  6928  ltexprlemloc  6929  ltexprlemfl  6931  ltexprlemfu  6933  prplnqu  6942  recexprlem1ssl  6955  recexprlem1ssu  6956  aptiprleml  6961  aptiprlemu  6962  caucvgprlemcanl  6966  cauappcvgprlemlol  6969  cauappcvgprlemloc  6974  cauappcvgprlemladdfu  6976  cauappcvgprlemladdru  6978  cauappcvgprlemladdrl  6979  cauappcvgprlem1  6981  caucvgprlemnkj  6988  caucvgprlemnbj  6989  caucvgprlemlol  6992  caucvgprlemloc  6997  caucvgprlemladdfu  6999  caucvgprlemladdrl  7000  caucvgprprlemnkltj  7011  caucvgprprlemnbj  7015  caucvgprprlemmu  7017  caucvgprprlemlol  7020  caucvgprprlemloc  7025  caucvgprprlemexbt  7028  caucvgprprlemexb  7029  caucvgprprlemaddq  7030  lttrsr  7071  ltsosr  7073  prsrlt  7095  caucvgsrlemoffcau  7106  caucvgsrlemoffgt1  7107  caucvgsrlemoffres  7108  caucvgsr  7110
  Copyright terms: Public domain W3C validator