On Wednesday, June 12, 2019 at 9:17:40 PM UTC+2, Jon P wrote: > > 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. >
Your first sentence is true, but it does not imply the second. In the case of itexp, you don't have the closed form "A -> B", but only the inference. There is no such straightforward way to get the deduction form from the inference form. In addition to Mario's slides I linked to above, you can have a look at http://us2.metamath.org/mpeuni/mmnatded.html and http://us2.metamath.org/mpeuni/mmdeduction.html -- 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/0e5c6872-4211-49b7-a272-1ee7c52263bb%40googlegroups.com.
