| Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > ILE Home > Th. List > spv | GIF version | ||
| Description: Specialization, using implicit substitition. (Contributed by NM, 30-Aug-1993.) |
| Ref | Expression |
|---|---|
| spv.1 | ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) |
| Ref | Expression |
|---|---|
| spv | ⊢ (∀𝑥𝜑 → 𝜓) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | spv.1 | . . 3 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) | |
| 2 | 1 | biimpd 144 | . 2 ⊢ (𝑥 = 𝑦 → (𝜑 → 𝜓)) |
| 3 | 2 | spimv 1833 | 1 ⊢ (∀𝑥𝜑 → 𝜓) |
| Colors of variables: wff set class |
| Syntax hints: → wi 4 ↔ wb 105 ∀wal 1370 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-5 1469 ax-gen 1471 ax-ie1 1515 ax-ie2 1516 ax-4 1532 ax-17 1548 ax-i9 1552 ax-ial 1556 |
| This theorem depends on definitions: df-bi 117 df-nf 1483 |
| This theorem is referenced by: spvv 1930 cbvalvw 1942 chvarv 1964 ru 2996 nalset 4173 tfisi 4633 tfr1onlemsucfn 6416 tfr1onlemsucaccv 6417 tfr1onlembxssdm 6419 tfr1onlembfn 6420 tfr1onlemres 6425 tfri1dALT 6427 tfrcllemsucfn 6429 tfrcllemsucaccv 6430 tfrcllembxssdm 6432 tfrcllembfn 6433 tfrcllemres 6438 findcard2 6968 findcard2s 6969 bj-nalset 15695 |
| Copyright terms: Public domain | W3C validator |