![]() |
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 1521 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | nfi 1439 |
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 105 ax-ia2 106 ax-ia3 107 ax-gen 1426 ax-ial 1515 |
This theorem depends on definitions: df-bi 116 df-nf 1438 |
This theorem is referenced by: nfnf1 1524 nfa2 1559 nfia1 1560 alexdc 1599 nf2 1647 cbv1h 1724 sbf2 1752 sb4or 1806 nfsbxy 1916 nfsbxyt 1917 sbcomxyyz 1946 sbalyz 1975 dvelimALT 1986 nfeu1 2011 moim 2064 euexex 2085 nfaba1 2288 nfra1 2469 ceqsalg 2717 elrab3t 2843 mo2icl 2867 csbie2t 3053 sbcnestgf 3056 dfss4st 3314 dfnfc2 3762 mpteq12f 4016 copsex2t 4175 ssopab2 4205 alxfr 4390 eunex 4484 mosubopt 4612 fv3 5452 fvmptt 5520 fnoprabg 5880 fiintim 6825 bj-exlimmp 13147 bdsepnft 13256 setindft 13334 strcollnft 13353 |
Copyright terms: Public domain | W3C validator |