Description: Show that the original axiom ax-c10 can be derived from ax6 and axc7 (on top of propositional calculus, ax-gen , and ax-4 ). See ax6fromc10 for the rederivation of ax6 from ax-c10 .
Normally, axc10 should be used rather than ax-c10 , except by theorems specifically studying the latter's properties. See bj-axc10v for a weaker version requiring fewer axioms. (Contributed by NM, 5-Aug-1993) (Proof modification is discouraged.) Usage of this theorem is discouraged because it depends on ax-13 . (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | axc10 | |- ( A. x ( x = y -> A. x ph ) -> ph ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | ax6 | |- -. A. x -. x = y |
|
| 2 | con3 | |- ( ( x = y -> A. x ph ) -> ( -. A. x ph -> -. x = y ) ) |
|
| 3 | 2 | al2imi | |- ( A. x ( x = y -> A. x ph ) -> ( A. x -. A. x ph -> A. x -. x = y ) ) |
| 4 | 1 3 | mtoi | |- ( A. x ( x = y -> A. x ph ) -> -. A. x -. A. x ph ) |
| 5 | axc7 | |- ( -. A. x -. A. x ph -> ph ) |
|
| 6 | 4 5 | syl | |- ( A. x ( x = y -> A. x ph ) -> ph ) |