| Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > ILE Home > Th. List > cnex | Unicode version | ||
| Description: Alias for ax-cnex 8018. (Contributed by Mario Carneiro, 17-Nov-2014.) |
| Ref | Expression |
|---|---|
| cnex |
|
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | ax-cnex 8018 |
1
|
| Colors of variables: wff set class |
| Syntax hints: |
| This theorem was proved from axioms: ax-cnex 8018 |
| This theorem is referenced by: reex 8061 cnelprrecn 8063 pnfnre 8116 mnfnre 8117 pnfxr 8127 nnex 9044 zex 9383 qex 9755 addex 9775 mulex 9776 ovshftex 11163 cndsex 14348 cnfldstr 14353 cnfldbas 14355 mpocnfldadd 14356 mpocnfldmul 14358 cnfldcj 14360 expghmap 14402 lmfval 14697 lmbrf 14720 lmfss 14749 lmres 14753 lmtopcnp 14755 cnmet 15035 cncfval 15077 elcncf 15078 limcrcl 15163 limccl 15164 ellimc3apf 15165 limccnp2lem 15181 limccnp2cntop 15182 reldvg 15184 dvfvalap 15186 dvbss 15190 dvidlemap 15196 dvidrelem 15197 dvidsslem 15198 dvcnp2cntop 15204 dvaddxxbr 15206 dvmulxxbr 15207 dvaddxx 15208 dvmulxx 15209 dviaddf 15210 dvimulf 15211 dvcoapbr 15212 dvcjbr 15213 dvcj 15214 dvfre 15215 dvexp 15216 dvrecap 15218 dvmptclx 15223 dvef 15232 plyval 15237 elply 15239 elply2 15240 plyf 15242 plyss 15243 elplyr 15245 plyaddlem1 15252 plymullem1 15253 plyaddlem 15254 plymullem 15255 plysub 15258 plycolemc 15263 plyco 15264 plycj 15266 |
| Copyright terms: Public domain | W3C validator |