metamath/valid/mathd-algebra-59.mm

$(
  @{
    mathd-algebra-59.0 @e |- ( ph -> B e. RR ) $@
    mathd-algebra-59.1 @e |- ( ph -> ( ( 4 ^ B ) + ( 2 ^ 3 ) ) = ; 1 2 ) $@
    @( (Contributed by Kunhao Zheng, 4-May-2021.) @)
    mathd-algebra-59 @p |- ( ph -> B = 1 ) @=
      ? @.
  @}
$)