| 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 1562 |
. 2
| |
| 2 | 1 | nfi 1484 |
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 1471 ax-ial 1556 |
| This theorem depends on definitions: df-bi 117 df-nf 1483 |
| This theorem is referenced by: axc4i 1564 nfnf1 1566 nfa2 1601 nfia1 1602 alexdc 1641 nf2 1690 cbv1h 1768 sbf2 1800 sb4or 1855 nfsbxy 1969 nfsbxyt 1970 sbcomxyyz 1999 sbalyz 2026 dvelimALT 2037 hbe1a 2050 nfeu1 2064 moim 2117 euexex 2138 nfaba1 2353 nfabdw 2366 nfra1 2536 ceqsalg 2799 elrab3t 2927 mo2icl 2951 csbie2t 3141 sbcnestgf 3144 dfss4st 3405 dfnfc2 3867 mpteq12f 4123 copsex2t 4288 ssopab2 4321 alxfr 4507 eunex 4608 mosubopt 4739 fv3 5598 fvmptt 5670 fnoprabg 6045 fiintim 7027 bj-exlimmp 15667 bdsepnft 15785 setindft 15863 strcollnft 15882 |
| Copyright terms: Public domain | W3C validator |