Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > addid1d | Unicode version |
Description: is an additive identity. (Contributed by Mario Carneiro, 27-May-2016.) |
Ref | Expression |
---|---|
muld.1 |
Ref | Expression |
---|---|
addid1d |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | muld.1 | . 2 | |
2 | addid1 7893 | . 2 | |
3 | 1, 2 | syl 14 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wceq 1331 wcel 1480 (class class class)co 5767 cc 7611 cc0 7613 caddc 7616 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-0id 7721 |
This theorem is referenced by: subsub2 7983 negsub 8003 ltaddneg 8179 ltaddpos 8207 addge01 8227 add20 8229 apreap 8342 nnge1 8736 nnnn0addcl 9000 un0addcl 9003 peano2z 9083 zaddcl 9087 uzaddcl 9374 xaddid1 9638 fzosubel3 9966 expadd 10328 faclbnd6 10483 omgadd 10541 reim0b 10627 rereb 10628 immul2 10645 resqrexlemcalc3 10781 resqrexlemnm 10783 max0addsup 10984 fsumsplit 11169 sumsplitdc 11194 bezoutlema 11676 cosmpi 12886 sinppi 12887 sinhalfpip 12890 trilpolemlt1 13223 |
Copyright terms: Public domain | W3C validator |