theorem powereqd (_G: wff) (_a1 _a2: nat): $ _G -> _a1 = _a2 $ > $ _G -> power _a1 = power _a2 $;
Step | Hyp | Ref | Expression |
---|---|---|---|
1 |
hyp _ah |
_G -> _a1 = _a2 |
|
2 |
_G -> _a1 == _a2 |
||
3 |
_G -> Power _a1 == Power _a2 |
||
4 |
_G -> lower (Power _a1) = lower (Power _a2) |
||
5 |
conv power |
_G -> power _a1 = power _a2 |