Description: Alternate proof of bj-ax12v3 . Uses axc11r and axc15 instead of ax-12 . (Contributed by BJ, 6-Jul-2021) (Proof modification is discouraged.) (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | bj-ax12v3ALT | |- ( x = y -> ( ph -> A. x ( x = y -> ph ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | ax-5 | |- ( ph -> A. y ph ) |
|
| 2 | axc11r | |- ( A. x x = y -> ( A. y ph -> A. x ph ) ) |
|
| 3 | ala1 | |- ( A. x ph -> A. x ( x = y -> ph ) ) |
|
| 4 | 1 2 3 | syl56 | |- ( A. x x = y -> ( ph -> A. x ( x = y -> ph ) ) ) |
| 5 | 4 | a1d | |- ( A. x x = y -> ( x = y -> ( ph -> A. x ( x = y -> ph ) ) ) ) |
| 6 | axc15 | |- ( -. A. x x = y -> ( x = y -> ( ph -> A. x ( x = y -> ph ) ) ) ) |
|
| 7 | 5 6 | pm2.61i | |- ( x = y -> ( ph -> A. x ( x = y -> ph ) ) ) |