![]() |
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 1466 |
. 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 105 ax-4 1455 |
This theorem depends on definitions: df-bi 116 df-nf 1405 |
This theorem is referenced by: alimd 1469 alrimi 1470 nfd 1471 nfrimi 1473 nfbidf 1487 19.3 1501 nfan1 1511 nfim1 1518 nfor 1521 nfal 1523 nfimd 1532 exlimi 1541 exlimd 1544 eximd 1559 albid 1562 exbid 1563 nfex 1584 19.9 1591 nf2 1614 nf3 1615 spim 1684 cbv2 1693 cbval 1695 cbvex 1697 nfald 1701 nfexd 1702 sbf 1718 nfs1f 1721 sbied 1729 sbie 1732 nfs1 1748 equs5or 1769 sb4or 1772 sbid2 1789 cbvexd 1862 hbsb 1883 sbco2yz 1897 sbco2 1899 sbco3v 1903 sbcomxyyz 1906 nfsbd 1911 hbeu 1981 mo23 2001 mor 2002 eu2 2004 eu3 2006 mo2r 2012 mo3 2014 mo2dc 2015 moexexdc 2044 nfsab 2092 nfcrii 2233 bj-sbime 12562 |
Copyright terms: Public domain | W3C validator |