| Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > ILE Home > Th. List > cnex | Unicode version | ||
| Description: Alias for ax-cnex 8123. (Contributed by Mario Carneiro, 17-Nov-2014.) |
| Ref | Expression |
|---|---|
| cnex |
|
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | ax-cnex 8123 |
1
|
| Colors of variables: wff set class |
| Syntax hints: |
| This theorem was proved from axioms: ax-cnex 8123 |
| This theorem is referenced by: reex 8166 cnelprrecn 8168 pnfnre 8221 mnfnre 8222 pnfxr 8232 nnex 9149 zex 9488 qex 9866 addex 9886 mulex 9887 ovshftex 11397 cndsex 14586 cnfldstr 14591 cnfldbas 14593 mpocnfldadd 14594 mpocnfldmul 14596 cnfldcj 14598 expghmap 14640 lmfval 14936 lmbrf 14958 lmfss 14987 lmres 14991 lmtopcnp 14993 cnmet 15273 cncfval 15315 elcncf 15316 limcrcl 15401 limccl 15402 ellimc3apf 15403 limccnp2lem 15419 limccnp2cntop 15420 reldvg 15422 dvfvalap 15424 dvbss 15428 dvidlemap 15434 dvidrelem 15435 dvidsslem 15436 dvcnp2cntop 15442 dvaddxxbr 15444 dvmulxxbr 15445 dvaddxx 15446 dvmulxx 15447 dviaddf 15448 dvimulf 15449 dvcoapbr 15450 dvcjbr 15451 dvcj 15452 dvfre 15453 dvexp 15454 dvrecap 15456 dvmptclx 15461 dvef 15470 plyval 15475 elply 15477 elply2 15478 plyf 15480 plyss 15481 elplyr 15483 plyaddlem1 15490 plymullem1 15491 plyaddlem 15492 plymullem 15493 plysub 15496 plycolemc 15501 plyco 15502 plycj 15504 |
| Copyright terms: Public domain | W3C validator |