$(
  @{
    @( (Contributed by Kunhao Zheng, 4-May-2021.) @)
    mathd-algebra-22 @p |- ( ph -> ( ( 5 ^ 2 ) logb ( 5 ^ 4 ) ) = 2 ) @=
      ? @.
  @}
$)