![]() |
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 1430 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | nfi 1348 |
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 99 ax-ia2 100 ax-ia3 101 ax-gen 1335 ax-ial 1424 |
This theorem depends on definitions: df-bi 110 df-nf 1347 |
This theorem is referenced by: nfnf1 1433 nfa2 1468 nfia1 1469 alexdc 1507 nf2 1555 cbv1h 1630 sbf2 1658 sb4or 1711 nfsbxy 1815 nfsbxyt 1816 sbcomxyyz 1843 sbalyz 1872 dvelimALT 1883 nfeu1 1908 moim 1961 euexex 1982 nfaba1 2180 nfra1 2349 ceqsalg 2576 elrab3t 2691 mo2icl 2714 csbie2t 2888 sbcnestgf 2891 dfnfc2 3589 mpteq12f 3828 copsex2t 3973 ssopab2 4003 alxfr 4159 eunex 4239 mosubopt 4348 fv3 5140 fvmptt 5205 fnoprabg 5544 bj-exlimmp 9244 bdsepnft 9342 setindft 9425 strcollnft 9444 |
Copyright terms: Public domain | W3C validator |