metamath/valid/mathd-algebra-48.mm

$(
  @{
    mathd-algebra-48.0 @e |- ( ph -> Q = ( 9 - ( 4 x. _i ) ) ) $@
    mathd-algebra-48.1 @e |- ( ph -> E = ( -u 3 - ( 4 x. _i ) ) ) $@
    @( (Contributed by Kunhao Zheng, 4-May-2021.) @)
    mathd-algebra-48 @p |- ( ph -> ( Q - E ) = ; 1 2 ) @=
      ? @.
  @}
$)