![]() |
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 1408 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | ax-mp 7 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 ax-4 1397 |
This theorem depends on definitions: df-bi 110 df-nf 1347 |
This theorem is referenced by: alimd 1411 alrimi 1412 nfd 1413 nfrimi 1415 nfbidf 1429 19.3 1443 nfan1 1453 nfim1 1460 nfor 1463 nfal 1465 nfimd 1474 exlimi 1482 exlimd 1485 eximd 1500 albid 1503 exbid 1504 nfex 1525 19.9 1532 nf2 1555 nf3 1556 spim 1623 cbv2 1632 cbval 1634 cbvex 1636 nfald 1640 nfexd 1641 sbf 1657 nfs1f 1660 sbied 1668 sbie 1671 nfs1 1687 equs5or 1708 sb4or 1711 sbid2 1727 cbvexd 1799 hbsb 1820 sbco2yz 1834 sbco2 1836 sbco3v 1840 sbcomxyyz 1843 nfsbd 1848 hbeu 1918 mo23 1938 mor 1939 eu2 1941 eu3 1943 mo2r 1949 mo3 1951 mo2dc 1952 moexexdc 1981 nfsab 2029 nfcrii 2168 bj-sbime 9248 |
Copyright terms: Public domain | W3C validator |