Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > nfri | GIF version |
Description: Consequence of the definition of not-free. (Contributed by Mario Carneiro, 11-Aug-2016.) |
Ref | Expression |
---|---|
nfri.1 | ⊢ Ⅎ𝑥𝜑 |
Ref | Expression |
---|---|
nfri | ⊢ (𝜑 → ∀𝑥𝜑) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfri.1 | . 2 ⊢ Ⅎ𝑥𝜑 | |
2 | nfr 1483 | . 2 ⊢ (Ⅎ𝑥𝜑 → (𝜑 → ∀𝑥𝜑)) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ (𝜑 → ∀𝑥𝜑) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∀wal 1314 Ⅎwnf 1421 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-4 1472 |
This theorem depends on definitions: df-bi 116 df-nf 1422 |
This theorem is referenced by: alimd 1486 alrimi 1487 nfd 1488 nfrimi 1490 nfbidf 1504 19.3 1518 nfan1 1528 nfim1 1535 nfor 1538 nfal 1540 nfimd 1549 exlimi 1558 exlimd 1561 eximd 1576 albid 1579 exbid 1580 nfex 1601 19.9 1608 nf2 1631 nf3 1632 spim 1701 cbv2 1710 cbval 1712 cbvex 1714 nfald 1718 nfexd 1719 sbf 1735 nfs1f 1738 sbied 1746 sbie 1749 nfs1 1765 equs5or 1786 sb4or 1789 sbid2 1806 cbvexd 1879 hbsb 1900 sbco2yz 1914 sbco2 1916 sbco3v 1920 sbcomxyyz 1923 nfsbd 1928 hbeu 1998 mo23 2018 mor 2019 eu2 2021 eu3 2023 mo2r 2029 mo3 2031 mo2dc 2032 moexexdc 2061 nfsab 2109 nfcrii 2251 bj-sbime 12907 |
Copyright terms: Public domain | W3C validator |