![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > cnex | Unicode version |
Description: Alias for ax-cnex 7901. (Contributed by Mario Carneiro, 17-Nov-2014.) |
Ref | Expression |
---|---|
cnex |
![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-cnex 7901 |
1
![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() |
This theorem was proved from axioms: ax-cnex 7901 |
This theorem is referenced by: reex 7944 cnelprrecn 7946 pnfnre 7997 mnfnre 7998 pnfxr 8008 nnex 8923 zex 9260 qex 9630 addex 9649 mulex 9650 ovshftex 10823 cnfldstr 13388 cnfldbas 13390 cnfldcj 13393 lmfval 13623 lmbrf 13646 lmfss 13675 lmres 13679 lmtopcnp 13681 cnmet 13961 cncfval 13990 elcncf 13991 limcrcl 14058 limccl 14059 ellimc3apf 14060 limccnp2lem 14076 limccnp2cntop 14077 reldvg 14079 dvfvalap 14081 dvbss 14085 dvidlemap 14091 dvcnp2cntop 14094 dvaddxxbr 14096 dvmulxxbr 14097 dvaddxx 14098 dvmulxx 14099 dviaddf 14100 dvimulf 14101 dvcoapbr 14102 dvcjbr 14103 dvcj 14104 dvfre 14105 dvexp 14106 dvrecap 14108 dvmptclx 14111 dvef 14119 |
Copyright terms: Public domain | W3C validator |