![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > nfa1 | Unicode version |
Description: ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
nfa1 |
![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | hba1 1485 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | nfi 1403 |
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-ia2 106 ax-ia3 107 ax-gen 1390 ax-ial 1479 |
This theorem depends on definitions: df-bi 116 df-nf 1402 |
This theorem is referenced by: nfnf1 1488 nfa2 1523 nfia1 1524 alexdc 1562 nf2 1610 cbv1h 1687 sbf2 1715 sb4or 1768 nfsbxy 1873 nfsbxyt 1874 sbcomxyyz 1901 sbalyz 1930 dvelimALT 1941 nfeu1 1966 moim 2019 euexex 2040 nfaba1 2241 nfra1 2420 ceqsalg 2661 elrab3t 2784 mo2icl 2808 csbie2t 2990 sbcnestgf 2993 dfss4st 3248 dfnfc2 3693 mpteq12f 3940 copsex2t 4096 ssopab2 4126 alxfr 4311 eunex 4405 mosubopt 4532 fv3 5363 fvmptt 5430 fnoprabg 5784 fiintim 6719 bj-exlimmp 12378 bdsepnft 12486 setindft 12568 strcollnft 12587 |
Copyright terms: Public domain | W3C validator |