en.wikipedia.org/wiki/Metamath
1 correction found
when you use the theorem opreq2i.
In the current Metamath Proof Explorer, that theorem is named `oveq2i`, not `opreq2i`; `opreq2i` is the old name.
Full reasoning
The current official Metamath Proof Explorer uses oveq2i for this proof step and explicitly notes that opreq2i was the older name. On the Metamath Proof Explorer home page, the walkthrough of the same 2p2e4 example says: Step 2 references theorem oveq2i “which used to be called opreq2i.” It also immediately continues by describing Step 2 as referencing the previously proved theorem oveq2i.
So the article's wording is outdated: in current set.mm, the theorem used in that example is oveq2i, while opreq2i is only the former name.
2 sources
- Proof Explorer - Home Page - Metamath
Figure 1. Step 2 of the 2p2e4 proof references step 1, which in turn "feeds" the hypothesis of earlier theorem oveq2i (which used to be called opreq2i).
- Proof Explorer - Home Page - Metamath
Look at Step 2 of the proof. In the Ref column, we see that it references a previously proved theorem, oveq2i.