| Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > ILE Home > Th. List > cnex | Unicode version | ||
| Description: Alias for ax-cnex 8051. (Contributed by Mario Carneiro, 17-Nov-2014.) |
| Ref | Expression |
|---|---|
| cnex |
|
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | ax-cnex 8051 |
1
|
| Colors of variables: wff set class |
| Syntax hints: |
| This theorem was proved from axioms: ax-cnex 8051 |
| This theorem is referenced by: reex 8094 cnelprrecn 8096 pnfnre 8149 mnfnre 8150 pnfxr 8160 nnex 9077 zex 9416 qex 9788 addex 9808 mulex 9809 ovshftex 11245 cndsex 14430 cnfldstr 14435 cnfldbas 14437 mpocnfldadd 14438 mpocnfldmul 14440 cnfldcj 14442 expghmap 14484 lmfval 14779 lmbrf 14802 lmfss 14831 lmres 14835 lmtopcnp 14837 cnmet 15117 cncfval 15159 elcncf 15160 limcrcl 15245 limccl 15246 ellimc3apf 15247 limccnp2lem 15263 limccnp2cntop 15264 reldvg 15266 dvfvalap 15268 dvbss 15272 dvidlemap 15278 dvidrelem 15279 dvidsslem 15280 dvcnp2cntop 15286 dvaddxxbr 15288 dvmulxxbr 15289 dvaddxx 15290 dvmulxx 15291 dviaddf 15292 dvimulf 15293 dvcoapbr 15294 dvcjbr 15295 dvcj 15296 dvfre 15297 dvexp 15298 dvrecap 15300 dvmptclx 15305 dvef 15314 plyval 15319 elply 15321 elply2 15322 plyf 15324 plyss 15325 elplyr 15327 plyaddlem1 15334 plymullem1 15335 plyaddlem 15336 plymullem 15337 plysub 15340 plycolemc 15345 plyco 15346 plycj 15348 |
| Copyright terms: Public domain | W3C validator |