Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > cnex | Unicode version |
Description: Alias for ax-cnex 7704. (Contributed by Mario Carneiro, 17-Nov-2014.) |
Ref | Expression |
---|---|
cnex |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-cnex 7704 | 1 |
Colors of variables: wff set class |
Syntax hints: wcel 1480 cvv 2681 cc 7611 |
This theorem was proved from axioms: ax-cnex 7704 |
This theorem is referenced by: reex 7747 cnelprrecn 7749 pnfnre 7800 mnfnre 7801 pnfxr 7811 nnex 8719 zex 9056 qex 9417 ovshftex 10584 lmfval 12350 lmbrf 12373 lmfss 12402 lmres 12406 lmtopcnp 12408 cnmet 12688 cncfval 12717 elcncf 12718 limcrcl 12785 limccl 12786 ellimc3apf 12787 limccnp2lem 12803 limccnp2cntop 12804 reldvg 12806 dvfvalap 12808 dvbss 12812 dvidlemap 12818 dvcnp2cntop 12821 dvaddxxbr 12823 dvmulxxbr 12824 dvaddxx 12825 dvmulxx 12826 dviaddf 12827 dvimulf 12828 dvcoapbr 12829 dvcjbr 12830 dvcj 12831 dvfre 12832 dvexp 12833 dvrecap 12835 dvmptclx 12838 dvef 12845 |
Copyright terms: Public domain | W3C validator |