metamath/valid/mathd-algebra-182.mm

$(
  @{
    mathd-algebra-182.0 @e |- ( ph -> Y e. CC ) $@
    @( (Contributed by Kunhao Zheng, 4-May-2021.) @)
    mathd-algebra-182 @p |- ( ph -> ( 7 x. ( ( 3 x. Y ) + 2 ) ) = ( ( ; 2 1 x. Y ) + ; 1 4 ) ) @=
      ? @.
  @}
$)