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 yy=xxφyφ

Proof

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