![]() |
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 7115 |
. 2
![]() ![]() | |
2 | cc 7111 |
. 2
![]() ![]() | |
3 | 1, 2 | wcel 1434 |
1
![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
This axiom is referenced by: 0cn 7243 mulid1 7248 cnegexlem2 7421 cnegex 7423 0cnALT 7435 negicn 7446 ine0 7635 ixi 7820 rimul 7822 rereim 7823 apreap 7824 cru 7839 apreim 7840 mulreim 7841 apadd1 7845 apneg 7848 recextlem1 7878 recexaplem2 7879 recexap 7880 crap0 8172 cju 8175 it0e0 8389 2mulicn 8390 iap0 8391 2muliap0 8392 cnref1o 8884 irec 9741 i2 9742 i3 9743 i4 9744 iexpcyc 9746 imval 9956 imre 9957 reim 9958 crre 9963 crim 9964 remim 9966 mulreap 9970 cjreb 9972 recj 9973 reneg 9974 readd 9975 remullem 9977 imcj 9981 imneg 9982 imadd 9983 cjadd 9990 cjneg 9996 imval2 10000 rei 10005 imi 10006 cji 10008 cjreim 10009 cjreim2 10010 cjap 10012 cnrecnv 10016 rennim 10107 absi 10164 absreimsq 10172 absreim 10173 absimle 10189 climcvg1nlem 10405 qdencn 11070 |
Copyright terms: Public domain | W3C validator |