![]() |
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 1551 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | nfi 1473 |
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 1460 ax-ial 1545 |
This theorem depends on definitions: df-bi 117 df-nf 1472 |
This theorem is referenced by: axc4i 1553 nfnf1 1555 nfa2 1590 nfia1 1591 alexdc 1630 nf2 1679 cbv1h 1757 sbf2 1789 sb4or 1844 nfsbxy 1954 nfsbxyt 1955 sbcomxyyz 1984 sbalyz 2011 dvelimALT 2022 hbe1a 2035 nfeu1 2049 moim 2102 euexex 2123 nfaba1 2338 nfabdw 2351 nfra1 2521 ceqsalg 2780 elrab3t 2907 mo2icl 2931 csbie2t 3120 sbcnestgf 3123 dfss4st 3383 dfnfc2 3842 mpteq12f 4098 copsex2t 4263 ssopab2 4293 alxfr 4479 eunex 4578 mosubopt 4709 fv3 5557 fvmptt 5628 fnoprabg 5997 fiintim 6957 bj-exlimmp 14979 bdsepnft 15097 setindft 15175 strcollnft 15194 |
Copyright terms: Public domain | W3C validator |