| Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > ILE Home > Th. List > cnex | Unicode version | ||
| Description: Alias for ax-cnex 8183. (Contributed by Mario Carneiro, 17-Nov-2014.) |
| Ref | Expression |
|---|---|
| cnex |
|
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | ax-cnex 8183 |
1
|
| Colors of variables: wff set class |
| Syntax hints: |
| This theorem was proved from axioms: ax-cnex 8183 |
| This theorem is referenced by: reex 8226 cnelprrecn 8228 pnfnre 8280 mnfnre 8281 pnfxr 8291 nnex 9208 zex 9549 qex 9927 addex 9947 mulex 9948 ovshftex 11459 cndsex 14649 cnfldstr 14654 cnfldbas 14656 mpocnfldadd 14657 mpocnfldmul 14659 cnfldcj 14661 expghmap 14703 lmfval 15004 lmbrf 15026 lmfss 15055 lmres 15059 lmtopcnp 15061 cnmet 15341 cncfval 15383 elcncf 15384 limcrcl 15469 limccl 15470 ellimc3apf 15471 limccnp2lem 15487 limccnp2cntop 15488 reldvg 15490 dvfvalap 15492 dvbss 15496 dvidlemap 15502 dvidrelem 15503 dvidsslem 15504 dvcnp2cntop 15510 dvaddxxbr 15512 dvmulxxbr 15513 dvaddxx 15514 dvmulxx 15515 dviaddf 15516 dvimulf 15517 dvcoapbr 15518 dvcjbr 15519 dvcj 15520 dvfre 15521 dvexp 15522 dvrecap 15524 dvmptclx 15529 dvef 15538 plyval 15543 elply 15545 elply2 15546 plyf 15548 plyss 15549 elplyr 15551 plyaddlem1 15558 plymullem1 15559 plyaddlem 15560 plymullem 15561 plysub 15564 plycolemc 15569 plyco 15570 plycj 15572 |
| Copyright terms: Public domain | W3C validator |