Metamath Proof Explorer


Theorem bm1.3iiOLD

Description: Obsolete version of sepexi as of 18-Sep-2025. (Contributed by NM, 21-Jun-1993) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypothesis bm1.3iiOLD.1 x y φ y x
Assertion bm1.3iiOLD x y y x φ

Proof

Step Hyp Ref Expression
1 bm1.3iiOLD.1 x y φ y x
2 19.42v x y φ y z y y x y z φ y φ y z x y y x y z φ
3 bimsc1 φ y z y x y z φ y x φ
4 3 alanimi y φ y z y y x y z φ y y x φ
5 4 eximi x y φ y z y y x y z φ x y y x φ
6 2 5 sylbir y φ y z x y y x y z φ x y y x φ
7 elequ2 x = z y x y z
8 7 imbi2d x = z φ y x φ y z
9 8 albidv x = z y φ y x y φ y z
10 9 cbvexvw x y φ y x z y φ y z
11 1 10 mpbi z y φ y z
12 ax-sep x y y x y z φ
13 11 12 exan z y φ y z x y y x y z φ
14 6 13 exlimiiv x y y x φ