| Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > ILE Home > Th. List > cnex | Unicode version | ||
| Description: Alias for ax-cnex 8101. (Contributed by Mario Carneiro, 17-Nov-2014.) |
| Ref | Expression |
|---|---|
| cnex |
|
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | ax-cnex 8101 |
1
|
| Colors of variables: wff set class |
| Syntax hints: |
| This theorem was proved from axioms: ax-cnex 8101 |
| This theorem is referenced by: reex 8144 cnelprrecn 8146 pnfnre 8199 mnfnre 8200 pnfxr 8210 nnex 9127 zex 9466 qex 9839 addex 9859 mulex 9860 ovshftex 11346 cndsex 14533 cnfldstr 14538 cnfldbas 14540 mpocnfldadd 14541 mpocnfldmul 14543 cnfldcj 14545 expghmap 14587 lmfval 14883 lmbrf 14905 lmfss 14934 lmres 14938 lmtopcnp 14940 cnmet 15220 cncfval 15262 elcncf 15263 limcrcl 15348 limccl 15349 ellimc3apf 15350 limccnp2lem 15366 limccnp2cntop 15367 reldvg 15369 dvfvalap 15371 dvbss 15375 dvidlemap 15381 dvidrelem 15382 dvidsslem 15383 dvcnp2cntop 15389 dvaddxxbr 15391 dvmulxxbr 15392 dvaddxx 15393 dvmulxx 15394 dviaddf 15395 dvimulf 15396 dvcoapbr 15397 dvcjbr 15398 dvcj 15399 dvfre 15400 dvexp 15401 dvrecap 15403 dvmptclx 15408 dvef 15417 plyval 15422 elply 15424 elply2 15425 plyf 15427 plyss 15428 elplyr 15430 plyaddlem1 15437 plymullem1 15438 plyaddlem 15439 plymullem 15440 plysub 15443 plycolemc 15448 plyco 15449 plycj 15451 |
| Copyright terms: Public domain | W3C validator |