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 7868 | . 2 | |
3 | 1, 2 | syl 14 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wceq 1316 wcel 1465 (class class class)co 5742 cc 7586 cc0 7588 caddc 7591 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-0id 7696 |
This theorem is referenced by: subsub2 7958 negsub 7978 ltaddneg 8154 ltaddpos 8182 addge01 8202 add20 8204 apreap 8317 nnge1 8711 nnnn0addcl 8975 un0addcl 8978 peano2z 9058 zaddcl 9062 uzaddcl 9349 xaddid1 9613 fzosubel3 9941 expadd 10303 faclbnd6 10458 omgadd 10516 reim0b 10602 rereb 10603 immul2 10620 resqrexlemcalc3 10756 resqrexlemnm 10758 max0addsup 10959 fsumsplit 11144 sumsplitdc 11169 bezoutlema 11614 cosmpi 12824 sinppi 12825 sinhalfpip 12828 trilpolemlt1 13161 |
Copyright terms: Public domain | W3C validator |