![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > nfi | GIF version |
Description: Deduce that x is not free in φ from the definition. (Contributed by Mario Carneiro, 11-Aug-2016.) |
Ref | Expression |
---|---|
nfi.1 | ⊢ (φ → ∀xφ) |
Ref | Expression |
---|---|
nfi | ⊢ Ⅎxφ |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-nf 1347 | . 2 ⊢ (Ⅎxφ ↔ ∀x(φ → ∀xφ)) | |
2 | nfi.1 | . 2 ⊢ (φ → ∀xφ) | |
3 | 1, 2 | mpgbir 1339 | 1 ⊢ Ⅎxφ |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∀wal 1240 Ⅎwnf 1346 |
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-gen 1335 |
This theorem depends on definitions: df-bi 110 df-nf 1347 |
This theorem is referenced by: nfth 1350 nfnth 1351 nfe1 1382 nfdh 1414 nfv 1418 nfa1 1431 nfan1 1453 nfim1 1460 nfor 1463 nfal 1465 nfex 1525 nfae 1604 cbv3h 1628 nfs1 1687 nfs1v 1812 hbsb 1820 sbco2h 1835 hbsbd 1855 dvelimALT 1883 dvelimfv 1884 hbeu 1918 hbeud 1919 eu3h 1942 mo3h 1950 nfsab1 2027 nfsab 2029 nfcii 2166 nfcri 2169 |
Copyright terms: Public domain | W3C validator |