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

Theorem caovord2d 5581
Description: Operation ordering law with commuted arguments. (Contributed by Mario Carneiro, 30-Dec-2014.)
Hypotheses
Ref Expression
caovordg.1 ((φ (x 𝑆 y 𝑆 z 𝑆)) → (x𝑅y ↔ (z𝐹x)𝑅(z𝐹y)))
caovordd.2 (φA 𝑆)
caovordd.3 (φB 𝑆)
caovordd.4 (φ𝐶 𝑆)
caovord2d.com ((φ (x 𝑆 y 𝑆)) → (x𝐹y) = (y𝐹x))
Assertion
Ref Expression
caovord2d (φ → (A𝑅B ↔ (A𝐹𝐶)𝑅(B𝐹𝐶)))
Distinct variable groups:   x,y,z,A   x,B,y,z   x,𝐶,y,z   φ,x,y,z   x,𝐹,y,z   x,𝑅,y,z   x,𝑆,y,z

Proof of Theorem caovord2d
StepHypRef Expression
1 caovordg.1 . . 3 ((φ (x 𝑆 y 𝑆 z 𝑆)) → (x𝑅y ↔ (z𝐹x)𝑅(z𝐹y)))
2 caovordd.2 . . 3 (φA 𝑆)
3 caovordd.3 . . 3 (φB 𝑆)
4 caovordd.4 . . 3 (φ𝐶 𝑆)
51, 2, 3, 4caovordd 5580 . 2 (φ → (A𝑅B ↔ (𝐶𝐹A)𝑅(𝐶𝐹B)))
6 caovord2d.com . . . 4 ((φ (x 𝑆 y 𝑆)) → (x𝐹y) = (y𝐹x))
76, 4, 2caovcomd 5568 . . 3 (φ → (𝐶𝐹A) = (A𝐹𝐶))
86, 4, 3caovcomd 5568 . . 3 (φ → (𝐶𝐹B) = (B𝐹𝐶))
97, 8breq12d 3740 . 2 (φ → ((𝐶𝐹A)𝑅(𝐶𝐹B) ↔ (A𝐹𝐶)𝑅(B𝐹𝐶)))
105, 9bitrd 177 1 (φ → (A𝑅B ↔ (A𝐹𝐶)𝑅(B𝐹𝐶)))
Colors of variables: wff set class
Syntax hints:  wi 4   wa 97  wb 98   w3a 867   = wceq 1223   wcel 1366   class class class wbr 3727  (class class class)co 5424
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-io 614  ax-5 1309  ax-7 1310  ax-gen 1311  ax-ie1 1355  ax-ie2 1356  ax-8 1368  ax-10 1369  ax-11 1370  ax-i12 1371  ax-bnd 1372  ax-4 1373  ax-17 1392  ax-i9 1396  ax-ial 1400  ax-i5r 1401  ax-ext 1995
This theorem depends on definitions:  df-bi 110  df-3an 869  df-tru 1226  df-nf 1323  df-sb 1619  df-clab 2000  df-cleq 2006  df-clel 2009  df-nfc 2140  df-ral 2280  df-rex 2281  df-v 2528  df-un 2890  df-sn 3345  df-pr 3346  df-op 3348  df-uni 3544  df-br 3728  df-iota 4782  df-fv 4825  df-ov 5427
This theorem is referenced by:  caovord3d  5582  genplt2i  6350  addnqprllem  6368  addnqprulem  6369  mulnqprl  6398  mulnqpru  6399  distrlem4prl  6409  distrlem4pru  6410  1idprl  6415  1idpru  6416  ltexprlemdisj  6429  ltexprlemloc  6430  ltexprlemfl  6432  ltexprlemfu  6434  recexprlem1ssl  6454  recexprlem1ssu  6455  aptiprleml  6460  aptiprlemu  6461  lttrsr  6500  ltsosr  6502
  Copyright terms: Public domain W3C validator