Description: A generalization of Axiom ax-c16 . Version of axc16g using ax-c11 . (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 | axc16g-o | |- ( A. x x = y -> ( ph -> A. z ph ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | aev-o | |- ( A. x x = y -> A. z z = x ) |
|
| 2 | ax-c16 | |- ( A. x x = y -> ( ph -> A. x ph ) ) |
|
| 3 | biidd | |- ( A. z z = x -> ( ph <-> ph ) ) |
|
| 4 | 3 | dral1-o | |- ( 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 ) ) |