![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > nfri | Unicode 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 1529 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | ax-mp 5 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-4 1521 |
This theorem depends on definitions: df-bi 117 df-nf 1472 |
This theorem is referenced by: alimd 1532 alrimi 1533 nfd 1534 nfrimi 1536 nfbidf 1550 19.3 1565 nfan1 1575 nfim1 1582 nfor 1585 nfimd 1596 exlimi 1605 exlimd 1608 eximd 1623 albid 1626 exbid 1627 nfex 1648 19.9 1655 nf2 1679 nf3 1680 spim 1749 cbv2 1760 cbvexv1 1763 cbval 1765 cbvex 1767 nfald 1771 nfexd 1772 sbf 1788 nfs1f 1791 sbied 1799 sbie 1802 nfs1 1820 equs5or 1841 sb4or 1844 sbid2 1861 cbvexd 1939 hbsb 1961 sbco2yz 1975 sbco2 1977 sbco3v 1981 sbcomxyyz 1984 nfsbd 1989 hbeu 2059 mo23 2079 mor 2080 eu2 2082 eu3 2084 mo2r 2090 mo3 2092 mo2dc 2093 moexexdc 2122 nfsab 2181 nfcrii 2325 bj-sbime 15003 |
Copyright terms: Public domain | W3C validator |