Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > cnex | Unicode version |
Description: Alias for ax-cnex 7835. (Contributed by Mario Carneiro, 17-Nov-2014.) |
Ref | Expression |
---|---|
cnex |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-cnex 7835 | 1 |
Colors of variables: wff set class |
Syntax hints: wcel 2135 cvv 2721 cc 7742 |
This theorem was proved from axioms: ax-cnex 7835 |
This theorem is referenced by: reex 7878 cnelprrecn 7880 pnfnre 7931 mnfnre 7932 pnfxr 7942 nnex 8854 zex 9191 qex 9561 ovshftex 10747 lmfval 12739 lmbrf 12762 lmfss 12791 lmres 12795 lmtopcnp 12797 cnmet 13077 cncfval 13106 elcncf 13107 limcrcl 13174 limccl 13175 ellimc3apf 13176 limccnp2lem 13192 limccnp2cntop 13193 reldvg 13195 dvfvalap 13197 dvbss 13201 dvidlemap 13207 dvcnp2cntop 13210 dvaddxxbr 13212 dvmulxxbr 13213 dvaddxx 13214 dvmulxx 13215 dviaddf 13216 dvimulf 13217 dvcoapbr 13218 dvcjbr 13219 dvcj 13220 dvfre 13221 dvexp 13222 dvrecap 13224 dvmptclx 13227 dvef 13235 |
Copyright terms: Public domain | W3C validator |