![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > cnex | Unicode version |
Description: Alias for ax-cnex 7965. (Contributed by Mario Carneiro, 17-Nov-2014.) |
Ref | Expression |
---|---|
cnex |
![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-cnex 7965 |
1
![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() |
This theorem was proved from axioms: ax-cnex 7965 |
This theorem is referenced by: reex 8008 cnelprrecn 8010 pnfnre 8063 mnfnre 8064 pnfxr 8074 nnex 8990 zex 9329 qex 9700 addex 9720 mulex 9721 ovshftex 10966 cndsex 14052 cnfldstr 14057 cnfldbas 14059 mpocnfldadd 14060 mpocnfldmul 14062 cnfldcj 14064 expghmap 14106 lmfval 14371 lmbrf 14394 lmfss 14423 lmres 14427 lmtopcnp 14429 cnmet 14709 cncfval 14751 elcncf 14752 limcrcl 14837 limccl 14838 ellimc3apf 14839 limccnp2lem 14855 limccnp2cntop 14856 reldvg 14858 dvfvalap 14860 dvbss 14864 dvidlemap 14870 dvidrelem 14871 dvidsslem 14872 dvcnp2cntop 14878 dvaddxxbr 14880 dvmulxxbr 14881 dvaddxx 14882 dvmulxx 14883 dviaddf 14884 dvimulf 14885 dvcoapbr 14886 dvcjbr 14887 dvcj 14888 dvfre 14889 dvexp 14890 dvrecap 14892 dvmptclx 14897 dvef 14906 plyval 14911 elply 14913 elply2 14914 plyf 14916 plyss 14917 elplyr 14919 plyaddlem1 14926 plymullem1 14927 plyaddlem 14928 plymullem 14929 plysub 14932 plycolemc 14936 plyco 14937 plycj 14939 |
Copyright terms: Public domain | W3C validator |