Description: Alternate proof of axc16g that uses df-sb and requires ax-10 , ax-11 , ax-13 . (Contributed by NM, 15-May-1993) (Proof shortened by Andrew Salmon, 25-May-2011) (Proof modification is discouraged.) (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | axc16gALT | |- ( A. x x = y -> ( ph -> A. z ph ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | aev | |- ( A. x x = y -> A. z z = x ) |
|
| 2 | axc16ALT | |- ( A. x x = y -> ( ph -> A. x ph ) ) |
|
| 3 | biidd | |- ( A. z z = x -> ( ph <-> ph ) ) |
|
| 4 | 3 | dral1 | |- ( A. z z = x -> ( A. z ph <-> A. x ph ) ) |
| 5 | 4 | biimprd | |- ( A. z z = x -> ( A. x ph -> A. z ph ) ) |
| 6 | 1 2 5 | sylsyld | |- ( A. x x = y -> ( ph -> A. z ph ) ) |