Promoting to the main body ad4ant* , ad5ant* and a couple more

[Glauco]

I've taken advantage of some theorems, still in mathboxes. Can I set up a PR for moving them to the main body?

Here's the list:

- supadd from Brendan Leahy's mathbox : sup distributes over addition (we already have supmul in the main part, that's "the same" for multiplication)

- inisegn0 from Stefan O'Rear's Mathbox : the comment says "Nonemptyness of an initial segment in terms of range" but it looks like it's more general than that, it's a nice and simple characterization of being

  an element of a range

- ad4ant* and ad5ant* from Alan Sare's Mathbox : these theorems allow to simplify complex antecedents; for instance, ad5ant245 selects three conditions out of five and saves three lines w.r.t

  syl3anc or syl21anc that would be an alternative solution. In the past, I've always refactored my proofs to avoid using these theorems, since they are not in the main body, but they would

  really shorten many of my proofs (and I'm pretty sure they could also shorten many other proofs in set.mm)

  

It there's consensus, I will submit a PR for promoting these theorems to the main part.

Glauco

[Norman Megill]

You have my approval.
Norm

[Jim Kingdon]

Add the ad4ant* and ad5ant* ones to iset.mm too if you have the time (if not, no worries, it can happen whenever someone gets around to it).

The supadd and inisegn0 ones wouldn't work in iset.mm.

--
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 metamath+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/e9fd83fb-4d2b-424b-b31a-0a6e6c65664co%40googlegroups.com.