![]() |
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 1411 |
. 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 1400 |
This theorem depends on definitions: df-bi 110 df-nf 1350 |
This theorem is referenced by: alimd 1414 alrimi 1415 nfd 1416 nfrimi 1418 nfbidf 1432 19.3 1446 nfan1 1456 nfim1 1463 nfor 1466 nfal 1468 nfimd 1477 exlimi 1485 exlimd 1488 eximd 1503 albid 1506 exbid 1507 nfex 1528 19.9 1535 nf2 1558 nf3 1559 spim 1626 cbv2 1635 cbval 1637 cbvex 1639 nfald 1643 nfexd 1644 sbf 1660 nfs1f 1663 sbied 1671 sbie 1674 nfs1 1690 equs5or 1711 sb4or 1714 sbid2 1730 cbvexd 1802 hbsb 1823 sbco2yz 1837 sbco2 1839 sbco3v 1843 sbcomxyyz 1846 nfsbd 1851 hbeu 1921 mo23 1941 mor 1942 eu2 1944 eu3 1946 mo2r 1952 mo3 1954 mo2dc 1955 moexexdc 1984 nfsab 2032 nfcrii 2171 bj-sbime 9913 |
Copyright terms: Public domain | W3C validator |