Description: Obsolete version of opabresex2 as of 13-Dec-2024. (Contributed by Alexander van der Vekens, 1-Nov-2017) (Revised by AV, 30-Dec-2020) (Proof shortened by AV, 15-Jan-2021) (New usage is discouraged.) (Proof modification is discouraged.)
Ref | Expression | ||
---|---|---|---|
Hypothesis | wlkResOLD.1 | ||
Assertion | wlkResOLD |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | wlkResOLD.1 | ||
2 | 1 | gen2 | |
3 | wksv | ||
4 | opabbrex | ||
5 | 2 3 4 | mp2an |