| Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > ILE Home > Th. List > cnex | Unicode version | ||
| Description: Alias for ax-cnex 8016. (Contributed by Mario Carneiro, 17-Nov-2014.) |
| Ref | Expression |
|---|---|
| cnex |
|
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | ax-cnex 8016 |
1
|
| Colors of variables: wff set class |
| Syntax hints: |
| This theorem was proved from axioms: ax-cnex 8016 |
| This theorem is referenced by: reex 8059 cnelprrecn 8061 pnfnre 8114 mnfnre 8115 pnfxr 8125 nnex 9042 zex 9381 qex 9753 addex 9773 mulex 9774 ovshftex 11130 cndsex 14315 cnfldstr 14320 cnfldbas 14322 mpocnfldadd 14323 mpocnfldmul 14325 cnfldcj 14327 expghmap 14369 lmfval 14664 lmbrf 14687 lmfss 14716 lmres 14720 lmtopcnp 14722 cnmet 15002 cncfval 15044 elcncf 15045 limcrcl 15130 limccl 15131 ellimc3apf 15132 limccnp2lem 15148 limccnp2cntop 15149 reldvg 15151 dvfvalap 15153 dvbss 15157 dvidlemap 15163 dvidrelem 15164 dvidsslem 15165 dvcnp2cntop 15171 dvaddxxbr 15173 dvmulxxbr 15174 dvaddxx 15175 dvmulxx 15176 dviaddf 15177 dvimulf 15178 dvcoapbr 15179 dvcjbr 15180 dvcj 15181 dvfre 15182 dvexp 15183 dvrecap 15185 dvmptclx 15190 dvef 15199 plyval 15204 elply 15206 elply2 15207 plyf 15209 plyss 15210 elplyr 15212 plyaddlem1 15219 plymullem1 15220 plyaddlem 15221 plymullem 15222 plysub 15225 plycolemc 15230 plyco 15231 plycj 15233 |
| Copyright terms: Public domain | W3C validator |