![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > nfi | GIF version |
Description: Deduce that 𝑥 is not free in 𝜑 from the definition. (Contributed by Mario Carneiro, 11-Aug-2016.) |
Ref | Expression |
---|---|
nfi.1 | ⊢ (𝜑 → ∀𝑥𝜑) |
Ref | Expression |
---|---|
nfi | ⊢ Ⅎ𝑥𝜑 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-nf 1438 | . 2 ⊢ (Ⅎ𝑥𝜑 ↔ ∀𝑥(𝜑 → ∀𝑥𝜑)) | |
2 | nfi.1 | . 2 ⊢ (𝜑 → ∀𝑥𝜑) | |
3 | 1, 2 | mpgbir 1430 | 1 ⊢ Ⅎ𝑥𝜑 |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∀wal 1330 Ⅎwnf 1437 |
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-gen 1426 |
This theorem depends on definitions: df-bi 116 df-nf 1438 |
This theorem is referenced by: nfth 1441 nfnth 1442 nfe1 1473 nfdh 1505 nfv 1509 nfa1 1522 nfan1 1544 nfim1 1551 nfor 1554 nfal 1556 nfex 1617 nfae 1698 cbv3h 1722 nfs1 1782 nfs1v 1913 hbsb 1923 sbco2h 1938 hbsbd 1958 dvelimALT 1986 dvelimfv 1987 hbeu 2021 hbeud 2022 eu3h 2045 mo3h 2053 nfsab1 2130 nfsab 2132 nfcii 2273 nfcri 2276 |
Copyright terms: Public domain | W3C validator |