Metamath Proof Explorer


Theorem relogbexpd

Description: Identity law for general logarithm: the logarithm of a power to the base is the exponent, a deduction version. (Contributed by metakunt, 22-May-2024)

Ref Expression
Hypotheses relogbexpd.1 φ B +
relogbexpd.2 φ B 1
relogbexpd.3 φ M
Assertion relogbexpd φ log B B M = M

Proof

Step Hyp Ref Expression
1 relogbexpd.1 φ B +
2 relogbexpd.2 φ B 1
3 relogbexpd.3 φ M
4 1 2 3 3jca φ B + B 1 M
5 relogbexp B + B 1 M log B B M = M
6 4 5 syl φ log B B M = M