metamath/valid/amc12b-2002-p11.mm

$(
  @{
    amc12b-2002-p11.0 @e |- ( ph -> A e. NN ) $@
    amc12b-2002-p11.1 @e |- ( ph -> B e. NN ) $@
    amc12b-2002-p11.2 @e |- ( ph -> A e. Prime ) $@
    amc12b-2002-p11.3 @e |- ( ph -> B e. Prime ) $@
    amc12b-2002-p11.4 @e |- ( ph -> ( A + B ) e. Prime ) $@
    amc12b-2002-p11.5 @e |- ( ph -> ( A - B ) e. Prime ) $@
    @( (Contributed by Kunhao Zheng, 4-May-2021.) @)
    amc12b-2002-p11 @p |- ( ph -> ( ( A + B ) + ( ( A - B ) + ( A + B ) ) ) e. Prime ) @=
      ? @.
  @}
$)