Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > cnex | Unicode version |
Description: Alias for ax-cnex 7679. (Contributed by Mario Carneiro, 17-Nov-2014.) |
Ref | Expression |
---|---|
cnex |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-cnex 7679 | 1 |
Colors of variables: wff set class |
Syntax hints: wcel 1465 cvv 2660 cc 7586 |
This theorem was proved from axioms: ax-cnex 7679 |
This theorem is referenced by: reex 7722 cnelprrecn 7724 pnfnre 7775 mnfnre 7776 pnfxr 7786 nnex 8694 zex 9031 qex 9392 ovshftex 10559 lmfval 12288 lmbrf 12311 lmfss 12340 lmres 12344 lmtopcnp 12346 cnmet 12626 cncfval 12655 elcncf 12656 limcrcl 12723 limccl 12724 ellimc3apf 12725 limccnp2lem 12741 limccnp2cntop 12742 reldvg 12744 dvfvalap 12746 dvbss 12750 dvidlemap 12756 dvcnp2cntop 12759 dvaddxxbr 12761 dvmulxxbr 12762 dvaddxx 12763 dvmulxx 12764 dviaddf 12765 dvimulf 12766 dvcoapbr 12767 dvcjbr 12768 dvcj 12769 dvfre 12770 dvexp 12771 dvrecap 12773 dvmptclx 12776 dvef 12783 |
Copyright terms: Public domain | W3C validator |