Description: The setvar x is not free in A. x ph . Example in Appendix in Megill p. 450 (p. 19 of the preprint). Also Lemma 22 of Monk2 p. 114. (Contributed by NM, 24-Jan-1993) (Proof modification is discouraged.) (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | hba1-o | |- ( A. x ph -> A. x A. x ph ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | ax-c5 | |- ( A. x -. A. x ph -> -. A. x ph ) |
|
| 2 | 1 | con2i | |- ( A. x ph -> -. A. x -. A. x ph ) |
| 3 | ax10fromc7 | |- ( -. A. x -. A. x ph -> A. x -. A. x -. A. x ph ) |
|
| 4 | ax10fromc7 | |- ( -. A. x ph -> A. x -. A. x ph ) |
|
| 5 | 4 | con1i | |- ( -. A. x -. A. x ph -> A. x ph ) |
| 6 | 5 | alimi | |- ( A. x -. A. x -. A. x ph -> A. x A. x ph ) |
| 7 | 2 3 6 | 3syl | |- ( A. x ph -> A. x A. x ph ) |