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

Theorem sb6f 1662
 Description: Equivalence for substitution when y is not free in φ. (Contributed by NM, 5-Aug-1993.) (Revised by NM, 30-Apr-2008.)
Hypothesis
Ref Expression
equs45f.1 (φyφ)
Assertion
Ref Expression
sb6f ([y / x]φx(x = yφ))

Proof of Theorem sb6f
StepHypRef Expression
1 equs45f.1 . . . 4 (φyφ)
21sbimi 1625 . . 3 ([y / x]φ → [y / x]yφ)
3 sb4a 1660 . . 3 ([y / x]yφx(x = yφ))
42, 3syl 14 . 2 ([y / x]φx(x = yφ))
5 sb2 1628 . 2 (x(x = yφ) → [y / x]φ)
64, 5impbii 117 1 ([y / x]φx(x = yφ))
 Colors of variables: wff set class Syntax hints:   → wi 4   ↔ wb 98  ∀wal 1224  [wsb 1623 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-5 1312  ax-gen 1314  ax-ie1 1359  ax-ie2 1360  ax-11 1374  ax-4 1377  ax-i9 1400  ax-ial 1405 This theorem depends on definitions:  df-bi 110  df-sb 1624 This theorem is referenced by:  sb5f  1663  sbcof2  1669
 Copyright terms: Public domain W3C validator