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

Theorem sbco2v 1863
 Description: This is a version of sbco2 1881 where 𝑧 is distinct from 𝑥. (Contributed by Jim Kingdon, 12-Feb-2018.)
Hypothesis
Ref Expression
sbco2v.1 (𝜑 → ∀𝑧𝜑)
Assertion
Ref Expression
sbco2v ([𝑦 / 𝑧][𝑧 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜑)
Distinct variable group:   𝑥,𝑧
Allowed substitution hints:   𝜑(𝑥,𝑦,𝑧)

Proof of Theorem sbco2v
Dummy variable 𝑤 is distinct from all other variables.
StepHypRef Expression
1 sbco2v.1 . . . 4 (𝜑 → ∀𝑧𝜑)
21sbco2vlem 1862 . . 3 ([𝑤 / 𝑧][𝑧 / 𝑥]𝜑 ↔ [𝑤 / 𝑥]𝜑)
32sbbii 1689 . 2 ([𝑦 / 𝑤][𝑤 / 𝑧][𝑧 / 𝑥]𝜑 ↔ [𝑦 / 𝑤][𝑤 / 𝑥]𝜑)
4 ax-17 1460 . . 3 ([𝑧 / 𝑥]𝜑 → ∀𝑤[𝑧 / 𝑥]𝜑)
54sbco2vlem 1862 . 2 ([𝑦 / 𝑤][𝑤 / 𝑧][𝑧 / 𝑥]𝜑 ↔ [𝑦 / 𝑧][𝑧 / 𝑥]𝜑)
6 ax-17 1460 . . 3 (𝜑 → ∀𝑤𝜑)
76sbco2vlem 1862 . 2 ([𝑦 / 𝑤][𝑤 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜑)
83, 5, 73bitr3i 208 1 ([𝑦 / 𝑧][𝑧 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜑)
 Colors of variables: wff set class Syntax hints:   → wi 4   ↔ wb 103  ∀wal 1283  [wsb 1686 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-4 1441  ax-17 1460  ax-i9 1464  ax-ial 1468  ax-i5r 1469 This theorem depends on definitions:  df-bi 115  df-nf 1391  df-sb 1687 This theorem is referenced by:  nfsb  1864  equsb3  1867  sbn  1868  sbim  1869  sbor  1870  sban  1871  sbco2vd  1883  sbco3v  1885  sbcom2v2  1904  sbcom2  1905  dfsb7  1909  sb7f  1910  sbal  1918  sbal1  1920  sbex  1922
 Copyright terms: Public domain W3C validator