Metamath Proof Explorer


Theorem elpwi2OLD

Description: Obsolete version of elpwi2 as of 26-May-2024. (Contributed by Glauco Siliprandi, 3-Mar-2021) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypotheses elpwi2.1 BV
elpwi2.2 AB
Assertion elpwi2OLD A𝒫B

Proof

Step Hyp Ref Expression
1 elpwi2.1 BV
2 elpwi2.2 AB
3 elpw2g BVA𝒫BAB
4 1 3 ax-mp A𝒫BAB
5 2 4 mpbir A𝒫B