On Monday, March 15, 2021 at 8:02:23 PM UTC+1 [email protected] wrote: > As an aside, it's much simpler to look at dedth instead, which uses an > explicit "if" expression instead of a combination of logical operators. I > think there were some plans to add "ifp" to set.mm but I guess it didn't > make it into the statement of this theorem. >
It is currently http://us.metamath.org/mpeuni/bj-dedthm.html I'd be happy to move it to Main. Benoît -- 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/7bbab395-bb4b-48cb-aee6-a4d23ea41dc3n%40googlegroups.com.
