Description: sp can be proven from the other classic axioms. (Contributed by Rohan Ridenour, 3-Nov-2023) (Proof modification is discouraged.) Use sp instead. (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | spALT | |- ( A. x ph -> ph ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | ax-1 | |- ( A. x ph -> ( x = y -> A. x ph ) ) |
|
| 2 | 1 | axc4i | |- ( A. x ph -> A. x ( x = y -> A. x ph ) ) |
| 3 | axc10 | |- ( A. x ( x = y -> A. x ph ) -> ph ) |
|
| 4 | 2 3 | syl | |- ( A. x ph -> ph ) |