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

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

Proof of Theorem sbco2vh
Dummy variable 𝑤 is distinct from all other variables.
StepHypRef Expression
1 sbco2vh.1 . . . 4 (𝜑 → ∀𝑧𝜑)
21sbco2vlem 1917 . . 3 ([𝑤 / 𝑧][𝑧 / 𝑥]𝜑 ↔ [𝑤 / 𝑥]𝜑)
32sbbii 1738 . 2 ([𝑦 / 𝑤][𝑤 / 𝑧][𝑧 / 𝑥]𝜑 ↔ [𝑦 / 𝑤][𝑤 / 𝑥]𝜑)
4 ax-17 1506 . . 3 ([𝑧 / 𝑥]𝜑 → ∀𝑤[𝑧 / 𝑥]𝜑)
54sbco2vlem 1917 . 2 ([𝑦 / 𝑤][𝑤 / 𝑧][𝑧 / 𝑥]𝜑 ↔ [𝑦 / 𝑧][𝑧 / 𝑥]𝜑)
6 ax-17 1506 . . 3 (𝜑 → ∀𝑤𝜑)
76sbco2vlem 1917 . 2 ([𝑦 / 𝑤][𝑤 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜑)
83, 5, 73bitr3i 209 1 ([𝑦 / 𝑧][𝑧 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜑)
 Colors of variables: wff set class Syntax hints:   → wi 4   ↔ wb 104  ∀wal 1329  [wsb 1735 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-io 698  ax-5 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-10 1483  ax-11 1484  ax-i12 1485  ax-4 1487  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515 This theorem depends on definitions:  df-bi 116  df-nf 1437  df-sb 1736 This theorem is referenced by:  nfsb  1919  equsb3  1924  sbn  1925  sbim  1926  sbor  1927  sban  1928  sbco2vd  1940  sbco3v  1942  sbcom2v2  1961  sbcom2  1962  dfsb7  1966  sb7f  1967  sbal  1975  sbal1  1977  sbex  1979
 Copyright terms: Public domain W3C validator