![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > nfi | Unicode version |
Description: Deduce that ![]() ![]() |
Ref | Expression |
---|---|
nfi.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
nfi |
![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-nf 1461 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | nfi.1 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | mpgbir 1453 |
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-ia2 107 ax-ia3 108 ax-gen 1449 |
This theorem depends on definitions: df-bi 117 df-nf 1461 |
This theorem is referenced by: nfth 1464 nfnth 1465 nfe1 1496 nfdh 1524 nfv 1528 nfa1 1541 nfan1 1564 nfim1 1571 nfor 1574 nfex 1637 nfae 1719 cbv3h 1743 nfs1 1809 nfs1v 1939 hbsb 1949 sbco2h 1964 hbsbd 1982 dvelimALT 2010 dvelimfv 2011 hbeu 2047 hbeud 2048 eu3h 2071 mo3h 2079 nfsab1 2167 nfsab 2169 nfcii 2310 nfcri 2313 |
Copyright terms: Public domain | W3C validator |