![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > addid1d | Unicode version |
Description: ![]() |
Ref | Expression |
---|---|
muld.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
addid1d |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | muld.1 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | addid1 7823 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | syl 14 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-0id 7653 |
This theorem is referenced by: subsub2 7913 negsub 7933 ltaddneg 8105 ltaddpos 8133 addge01 8153 add20 8155 apreap 8267 nnge1 8653 nnnn0addcl 8911 un0addcl 8914 peano2z 8994 zaddcl 8998 uzaddcl 9283 xaddid1 9538 fzosubel3 9866 expadd 10228 faclbnd6 10383 omgadd 10441 reim0b 10527 rereb 10528 immul2 10545 resqrexlemcalc3 10680 resqrexlemnm 10682 max0addsup 10883 fsumsplit 11068 sumsplitdc 11093 bezoutlema 11533 trilpolemlt1 12926 |
Copyright terms: Public domain | W3C validator |