oveq2i has logical hypothesis named oveq1i.1

[heiph...@wilsonb.com]

Hello,

The logical hypothesis for theorem oveq2i has the same name as that for oveq1i. This tripped me up, but is the naming intentional?

In particular, I was writing up my own proof of 2p2e4 when I noticed the clash. In fact, the proof of 2p2e4 exhibits the same exact issue: the first unification is oveq1i.1=df-2, which is followed by it's parent eqtr4i.1=oveq2i. Given that 2p2e4 is used as an pedagogical example in MPE, I feel like I must just be missing something obvious.

Just in case, I also confirmed the above against HEAD on the develop branch (commit 2ebe15d3 at the time).

Forgive the spam if I am just overlooking something

Cheers,
B. Wilson

[Jim Kingdon]

This is relatively common when people want related theorems to have the
same hypothesis.

If you look at set.mm, you'll see that oveq1i.1 only appears once, but
in a ${ $} block which includes both oveq1i and oveq2i .

[B. Wilson]

Excellent. So I just happened to stumble upon a nice method used to organize related deductions. Much appreciated.

> --
> 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/eddf8e5b-8733-4ebd-26fd-598253221bb3%40panix.com.

[heiph...@wilsonb.com]

[Mario Carneiro]

Our hopes and prayers go out to B. Wilson, that he may one day escape his time loop.

(I think it was a moderation error leading to the email getting resent.)

Mario

--
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/20191026084856.GF24895%40lang.