I think you convinced me that there are not many cases like fsumshft, and there are even less situations for such theorems in which the antecedent ph is useful in a hypothesis. Therefore, we can end the discussion here. If I find a similar case in the future, I will revise the theorem/proof accordingly (because thanks to Norm I know how it can be done).
> -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/7fe6094b-95a9-442f-b9ae-b8b80cb7c59a%40googlegroups.com.
