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 1511 | . 2 ⊢ (Ⅎ𝑥𝜑 → (𝜑 → ∀𝑥𝜑)) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ (𝜑 → ∀𝑥𝜑) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∀wal 1346 Ⅎwnf 1453 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-4 1503 |
This theorem depends on definitions: df-bi 116 df-nf 1454 |
This theorem is referenced by: alimd 1514 alrimi 1515 nfd 1516 nfrimi 1518 nfbidf 1532 19.3 1547 nfan1 1557 nfim1 1564 nfor 1567 nfimd 1578 exlimi 1587 exlimd 1590 eximd 1605 albid 1608 exbid 1609 nfex 1630 19.9 1637 nf2 1661 nf3 1662 spim 1731 cbv2 1742 cbvexv1 1745 cbval 1747 cbvex 1749 nfald 1753 nfexd 1754 sbf 1770 nfs1f 1773 sbied 1781 sbie 1784 nfs1 1802 equs5or 1823 sb4or 1826 sbid2 1843 cbvexd 1920 hbsb 1942 sbco2yz 1956 sbco2 1958 sbco3v 1962 sbcomxyyz 1965 nfsbd 1970 hbeu 2040 mo23 2060 mor 2061 eu2 2063 eu3 2065 mo2r 2071 mo3 2073 mo2dc 2074 moexexdc 2103 nfsab 2162 nfcrii 2305 bj-sbime 13729 |
Copyright terms: Public domain | W3C validator |