![]() |
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 1472 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | nfi.1 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | mpgbir 1464 |
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 1460 |
This theorem depends on definitions: df-bi 117 df-nf 1472 |
This theorem is referenced by: nfth 1475 nfnth 1476 nfe1 1507 nfdh 1535 nfv 1539 nfa1 1552 nfan1 1575 nfim1 1582 nfor 1585 nfex 1648 nfae 1730 cbv3h 1754 nfs1 1820 nfs1v 1951 hbsb 1961 sbco2h 1976 hbsbd 1994 dvelimALT 2022 dvelimfv 2023 hbeu 2059 hbeud 2060 eu3h 2083 mo3h 2091 nfsab1 2179 nfsab 2181 nfcii 2323 nfcri 2326 |
Copyright terms: Public domain | W3C validator |