metamath/valid/mathd-numbertheory-101.mm

$(
  @{
    @( (Contributed by Kunhao Zheng, 4-May-2021.) @)
    mathd-numbertheory-101 @p |- ( ph -> ( ( ; 1 7 x. ; 1 8 ) mod 4 ) = 2 ) @=
      ? @.
  @}
$)