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 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax12 | |
|
2 | 1 | sps | |
3 | pm2.27 | |
|
4 | 3 | al2imi | |
5 | 2 4 | syld | |