![]() |
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 2332 |
. 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 106 ax-ia2 107 ax-ia3 108 ax-gen 1460 ax-17 1537 |
This theorem depends on definitions: df-bi 117 df-nf 1472 df-nfc 2321 |
This theorem is referenced by: nfeld 2348 nfraldw 2522 vtoclgft 2802 vtocld 2804 sbcralt 3054 sbcrext 3055 csbied 3118 csbie2t 3120 sbcco3g 3129 csbco3g 3130 dfnfc2 3842 eusvnfb 4469 eusv2i 4470 peano2 4609 iota2d 5218 iota2 5221 fmptcof 5699 riota5f 5871 riota5 5872 fmpoco 6235 nfixpxy 6735 nfnegd 8171 iseqf1olemjpcl 10513 iseqf1olemqpcl 10514 iseqf1olemfvp 10515 seq3f1olemqsum 10518 fprodeq0g 11664 pcmpt 12359 strcollnft 15133 |
Copyright terms: Public domain | W3C validator |