![]() |
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 8098 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | syl 14 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-0id 7922 |
This theorem is referenced by: subsub2 8188 negsub 8208 ltaddneg 8384 ltaddpos 8412 addge01 8432 add20 8434 apreap 8547 nnge1 8945 nnnn0addcl 9209 un0addcl 9212 peano2z 9292 zaddcl 9296 uzaddcl 9589 xaddid1 9865 fzosubel3 10199 expadd 10565 faclbnd6 10727 omgadd 10785 reim0b 10874 rereb 10875 immul2 10892 resqrexlemcalc3 11028 resqrexlemnm 11030 max0addsup 11231 fsumsplit 11418 sumsplitdc 11443 bezoutlema 12003 pcadd 12342 pcmpt 12344 mulgnn0dir 13019 cosmpi 14377 sinppi 14378 sinhalfpip 14381 trilpolemlt1 14929 |
Copyright terms: Public domain | W3C validator |