>From my understanding the non-trivial case is when you have Ti, but neither T nor Td. I think most theorems in the set.mm database have a deductive or closed form somewhere, but you might have to use a proof assistance tool to search based on the form if the name isn't obvious. When writing your own theorems/lemmas you should always put an arbitrary antecedent before every hypothesis so you are always in deductive form. To use a deductive form theorem you need to first obtain matching antecedents for each hypothesis used. You can use "a1i" to add antecedents to the left hand side, then use "imp" or "exp" to convert chained antecedents into conjunctions that you can change the order of using commutative and associative properties. On Tuesday, August 15, 2023 at 11:41:48 AM UTC-4 [email protected] wrote:
> Thanks a lot! > > Also, the website states: > > "As noted earlier, we can also easily convert any assertion T in closed > form to its related assertion Ti in inference form by applying ax-mp > <https://us.metamath.org/mpeuni/ax-mp.html>. The challenge, when working > formally, can sometimes occur when converting some arbitrary assertion T in > inference form into a related assertion Td in deduction form" > > Still, are there some examples or are there general guidelines that will > help with this process? How would I go about converting Ti to Td in the > example stated above (or from Ti to T)? > > Again, many thanks! > Op dinsdag 15 augustus 2023 om 17:02:33 UTC+2 schreef [email protected]: > >> On 8/15/23 07:49, David A. Wheeler wrote: >> > Maybe we should note something in trud. >> >> Ooh, good idea. I hadn't thought of that as a mitigation. Submitted as >> https://github.com/metamath/set.mm/pull/3388 >> >> >> -- 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/cad028d6-7d21-40be-866c-1531e7fac313n%40googlegroups.com.
