![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > nfcvd | Unicode version |
Description: If ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
nfcvd |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfcv 2282 |
. 2
![]() ![]() ![]() ![]() | |
2 | 1 | a1i 9 |
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-17 1507 |
This theorem depends on definitions: df-bi 116 df-nf 1438 df-nfc 2271 |
This theorem is referenced by: nfeld 2298 vtoclgft 2739 vtocld 2741 sbcralt 2989 sbcrext 2990 csbied 3051 csbie2t 3053 sbcco3g 3062 csbco3g 3063 dfnfc2 3762 eusvnfb 4383 eusv2i 4384 peano2 4517 iota2d 5121 iota2 5122 fmptcof 5595 riota5f 5762 riota5 5763 fmpoco 6121 nfixpxy 6619 nfnegd 7982 iseqf1olemjpcl 10299 iseqf1olemqpcl 10300 iseqf1olemfvp 10301 seq3f1olemqsum 10304 strcollnft 13353 |
Copyright terms: Public domain | W3C validator |