Hi! I think there is a general trick to replace a $d x A or $d x ph$ condition in a theorem with the corresponding F/_ x A or F/ x ph, but I do not remember it. Can anybody help me?
(in this specific case, I would like to do that for sbcex2 and its universal counterpart) Thanks, Giovanni. PS. I already asked the same question on the Metamath Gitter channel[1], but I believe it is not very active at the moment! [1] https://gitter.im/metamath/Lobby -- Giovanni Mascellani <[email protected]> Postdoc researcher - Université Libre de Bruxelles -- 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/c1751381-622c-a19b-9054-cb6f48d94f33%40gmail.com.
signature.asc
Description: OpenPGP digital signature
