![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > ax-icn | Unicode version |
Description: ![]() |
Ref | Expression |
---|---|
ax-icn |
![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ci 7812 |
. 2
![]() ![]() | |
2 | cc 7808 |
. 2
![]() ![]() | |
3 | 1, 2 | wcel 2148 |
1
![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
This axiom is referenced by: 0cn 7948 mulrid 7953 cnegexlem2 8131 cnegex 8133 0cnALT 8145 negicn 8156 ine0 8349 ixi 8538 rimul 8540 rereim 8541 apreap 8542 cru 8557 apreim 8558 mulreim 8559 apadd1 8563 apneg 8566 aprcl 8601 aptap 8605 recextlem1 8606 recexaplem2 8607 recexap 8608 crap0 8913 cju 8916 it0e0 9138 2mulicn 9139 iap0 9140 2muliap0 9141 cnref1o 9648 irec 10616 i2 10617 i3 10618 i4 10619 iexpcyc 10621 imval 10854 imre 10855 reim 10856 crre 10861 crim 10862 remim 10864 mulreap 10868 cjreb 10870 recj 10871 reneg 10872 readd 10873 remullem 10875 imcj 10879 imneg 10880 imadd 10881 cjadd 10888 cjneg 10894 imval2 10898 rei 10903 imi 10904 cji 10906 cjreim 10907 cjreim2 10908 cjap 10910 cnrecnv 10914 rennim 11006 absi 11063 absreimsq 11071 absreim 11072 absimle 11088 climcvg1nlem 11352 sinval 11705 cosval 11706 sinf 11707 cosf 11708 tanval2ap 11716 tanval3ap 11717 resinval 11718 recosval 11719 efi4p 11720 resin4p 11721 recos4p 11722 resincl 11723 recoscl 11724 sinneg 11729 cosneg 11730 efival 11735 efmival 11736 efeul 11737 sinadd 11739 cosadd 11740 ef01bndlem 11759 sin01bnd 11760 cos01bnd 11761 absef 11772 absefib 11773 efieq1re 11774 demoivre 11775 demoivreALT 11776 igz 12366 cnrehmeocntop 13986 sincn 14083 coscn 14084 efhalfpi 14113 ef2kpi 14120 efper 14121 sinperlem 14122 efimpi 14133 2sqlem2 14344 qdencn 14657 |
Copyright terms: Public domain | W3C validator |