Description: Show that the original axiom ax-c7 can be derived from ax-10 ( hbn1 ) , sp and propositional calculus. See ax10fromc7 for the rederivation of ax-10 from ax-c7 .
Normally, axc7 should be used rather than ax-c7 , except by theorems specifically studying the latter's properties. (Contributed by NM, 21-May-2008)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | axc7 | |- ( -. A. x -. A. x ph -> ph ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | sp | |- ( A. x ph -> ph ) |
|
| 2 | hbn1 | |- ( -. A. x ph -> A. x -. A. x ph ) |
|
| 3 | 1 2 | nsyl4 | |- ( -. A. x -. A. x ph -> ph ) |