metamath/valid/mathd-numbertheory-132.mm

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