Re deduction form is there any way to create a general wrapper? I imagine you've considered this already.
If ( A -> B ) does that imply ( ( ph -> A ) -> ( ph -> B ) )? If so could I just prove the deduction version from the current version by adding that at the start? I think that might be possible. -- 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/9b6e97e7-0657-4faf-9b4a-7be66c6dbdcf%40googlegroups.com.
