| Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > ILE Home > Th. List > cnex | Unicode version | ||
| Description: Alias for ax-cnex 7970. (Contributed by Mario Carneiro, 17-Nov-2014.) |
| Ref | Expression |
|---|---|
| cnex |
|
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | ax-cnex 7970 |
1
|
| Colors of variables: wff set class |
| Syntax hints: |
| This theorem was proved from axioms: ax-cnex 7970 |
| This theorem is referenced by: reex 8013 cnelprrecn 8015 pnfnre 8068 mnfnre 8069 pnfxr 8079 nnex 8996 zex 9335 qex 9706 addex 9726 mulex 9727 ovshftex 10984 cndsex 14109 cnfldstr 14114 cnfldbas 14116 mpocnfldadd 14117 mpocnfldmul 14119 cnfldcj 14121 expghmap 14163 lmfval 14428 lmbrf 14451 lmfss 14480 lmres 14484 lmtopcnp 14486 cnmet 14766 cncfval 14808 elcncf 14809 limcrcl 14894 limccl 14895 ellimc3apf 14896 limccnp2lem 14912 limccnp2cntop 14913 reldvg 14915 dvfvalap 14917 dvbss 14921 dvidlemap 14927 dvidrelem 14928 dvidsslem 14929 dvcnp2cntop 14935 dvaddxxbr 14937 dvmulxxbr 14938 dvaddxx 14939 dvmulxx 14940 dviaddf 14941 dvimulf 14942 dvcoapbr 14943 dvcjbr 14944 dvcj 14945 dvfre 14946 dvexp 14947 dvrecap 14949 dvmptclx 14954 dvef 14963 plyval 14968 elply 14970 elply2 14971 plyf 14973 plyss 14974 elplyr 14976 plyaddlem1 14983 plymullem1 14984 plyaddlem 14985 plymullem 14986 plysub 14989 plycolemc 14994 plyco 14995 plycj 14997 |
| Copyright terms: Public domain | W3C validator |