Metamath Proof Explorer


Theorem wl-axc11r

Description: Same as axc11r , but using ax12 instead of ax-12 directly. This better reflects axiom usage in theorems dependent on it. (Contributed by NM, 25-Jul-2015) Avoid direct use of ax-12 . (Revised by Wolf Lammen, 30-Mar-2024)

Ref Expression
Assertion wl-axc11r y y = x x φ y φ

Proof

Step Hyp Ref Expression
1 ax12 y = x x φ y y = x φ
2 1 sps y y = x x φ y y = x φ
3 pm2.27 y = x y = x φ φ
4 3 al2imi y y = x y y = x φ y φ
5 2 4 syld y y = x x φ y φ