| Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > ILE Home > Th. List > cnex | Unicode version | ||
| Description: Alias for ax-cnex 8090. (Contributed by Mario Carneiro, 17-Nov-2014.) |
| Ref | Expression |
|---|---|
| cnex |
|
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | ax-cnex 8090 |
1
|
| Colors of variables: wff set class |
| Syntax hints: |
| This theorem was proved from axioms: ax-cnex 8090 |
| This theorem is referenced by: reex 8133 cnelprrecn 8135 pnfnre 8188 mnfnre 8189 pnfxr 8199 nnex 9116 zex 9455 qex 9827 addex 9847 mulex 9848 ovshftex 11330 cndsex 14517 cnfldstr 14522 cnfldbas 14524 mpocnfldadd 14525 mpocnfldmul 14527 cnfldcj 14529 expghmap 14571 lmfval 14867 lmbrf 14889 lmfss 14918 lmres 14922 lmtopcnp 14924 cnmet 15204 cncfval 15246 elcncf 15247 limcrcl 15332 limccl 15333 ellimc3apf 15334 limccnp2lem 15350 limccnp2cntop 15351 reldvg 15353 dvfvalap 15355 dvbss 15359 dvidlemap 15365 dvidrelem 15366 dvidsslem 15367 dvcnp2cntop 15373 dvaddxxbr 15375 dvmulxxbr 15376 dvaddxx 15377 dvmulxx 15378 dviaddf 15379 dvimulf 15380 dvcoapbr 15381 dvcjbr 15382 dvcj 15383 dvfre 15384 dvexp 15385 dvrecap 15387 dvmptclx 15392 dvef 15401 plyval 15406 elply 15408 elply2 15409 plyf 15411 plyss 15412 elplyr 15414 plyaddlem1 15421 plymullem1 15422 plyaddlem 15423 plymullem 15424 plysub 15427 plycolemc 15432 plyco 15433 plycj 15435 |
| Copyright terms: Public domain | W3C validator |