![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > cnex | Unicode version |
Description: Alias for ax-cnex 7897. (Contributed by Mario Carneiro, 17-Nov-2014.) |
Ref | Expression |
---|---|
cnex |
![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-cnex 7897 |
1
![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() |
This theorem was proved from axioms: ax-cnex 7897 |
This theorem is referenced by: reex 7940 cnelprrecn 7942 pnfnre 7993 mnfnre 7994 pnfxr 8004 nnex 8919 zex 9256 qex 9626 addex 9645 mulex 9646 ovshftex 10819 cnfldstr 13262 cnfldbas 13264 cnfldcj 13267 lmfval 13474 lmbrf 13497 lmfss 13526 lmres 13530 lmtopcnp 13532 cnmet 13812 cncfval 13841 elcncf 13842 limcrcl 13909 limccl 13910 ellimc3apf 13911 limccnp2lem 13927 limccnp2cntop 13928 reldvg 13930 dvfvalap 13932 dvbss 13936 dvidlemap 13942 dvcnp2cntop 13945 dvaddxxbr 13947 dvmulxxbr 13948 dvaddxx 13949 dvmulxx 13950 dviaddf 13951 dvimulf 13952 dvcoapbr 13953 dvcjbr 13954 dvcj 13955 dvfre 13956 dvexp 13957 dvrecap 13959 dvmptclx 13962 dvef 13970 |
Copyright terms: Public domain | W3C validator |