metamath/valid/mathd-numbertheory-45.mm

$(
  @{
    @( (Contributed by Kunhao Zheng, 4-May-2021.) @)
    mathd-numbertheory-45 @p |- ( ph -> ( ( ; ; ; 6 4 3 2 gcd ; ; 1 3 2 ) + ; 1 1 ) = ; 2 3 ) @=
      ? @.
  @}
$)