| 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 1563 |
. 2
| |
| 2 | 1 | nfi 1485 |
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 1472 ax-ial 1557 |
| This theorem depends on definitions: df-bi 117 df-nf 1484 |
| This theorem is referenced by: axc4i 1565 nfnf1 1567 nfa2 1602 nfia1 1603 alexdc 1642 nf2 1691 cbv1h 1769 sbf2 1801 sb4or 1856 nfsbxy 1970 nfsbxyt 1971 sbcomxyyz 2000 sbalyz 2027 dvelimALT 2038 hbe1a 2051 nfeu1 2065 moim 2118 euexex 2139 nfaba1 2354 nfabdw 2367 nfra1 2537 ceqsalg 2800 elrab3t 2928 mo2icl 2952 csbie2t 3142 sbcnestgf 3145 dfss4st 3406 dfnfc2 3868 mpteq12f 4124 copsex2t 4289 ssopab2 4322 alxfr 4508 eunex 4609 mosubopt 4740 fv3 5599 fvmptt 5671 fnoprabg 6046 fiintim 7028 bj-exlimmp 15705 bdsepnft 15823 setindft 15901 strcollnft 15920 |
| Copyright terms: Public domain | W3C validator |