![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > sbieh | GIF version |
Description: Conversion of implicit substitution to explicit substitution. New proofs should use sbie 1671 instead. (Contributed by NM, 30-Jun-1994.) (New usage is discouraged.) |
Ref | Expression |
---|---|
sbieh.1 | ⊢ (ψ → ∀xψ) |
sbieh.2 | ⊢ (x = y → (φ ↔ ψ)) |
Ref | Expression |
---|---|
sbieh | ⊢ ([y / x]φ ↔ ψ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | id 19 | . 2 ⊢ (φ → φ) | |
2 | 1 | hbth 1349 | . . 3 ⊢ ((φ → φ) → ∀x(φ → φ)) |
3 | sbieh.1 | . . . 4 ⊢ (ψ → ∀xψ) | |
4 | 3 | a1i 9 | . . 3 ⊢ ((φ → φ) → (ψ → ∀xψ)) |
5 | sbieh.2 | . . . 4 ⊢ (x = y → (φ ↔ ψ)) | |
6 | 5 | a1i 9 | . . 3 ⊢ ((φ → φ) → (x = y → (φ ↔ ψ))) |
7 | 2, 4, 6 | sbiedh 1667 | . 2 ⊢ ((φ → φ) → ([y / x]φ ↔ ψ)) |
8 | 1, 7 | ax-mp 7 | 1 ⊢ ([y / x]φ ↔ ψ) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ↔ wb 98 ∀wal 1240 [wsb 1642 |
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 1333 ax-gen 1335 ax-ie1 1379 ax-ie2 1380 ax-4 1397 ax-i9 1420 ax-ial 1424 |
This theorem depends on definitions: df-bi 110 df-sb 1643 |
This theorem is referenced by: sbie 1671 sbco2vlem 1817 equsb3lem 1821 sbco2yz 1834 elsb3 1849 elsb4 1850 dvelimf 1888 |
Copyright terms: Public domain | W3C validator |