Description: Deduction form of Theorem 19.20 of Margaris p. 90, see alim . See alimdh and alimd for versions without a distinct variable condition. (Contributed by NM, 3-Apr-1994)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | alimdv.1 | |- ( ph -> ( ps -> ch ) ) |
|
| Assertion | alimdv | |- ( ph -> ( A. x ps -> A. x ch ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | alimdv.1 | |- ( ph -> ( ps -> ch ) ) |
|
| 2 | ax-5 | |- ( ph -> A. x ph ) |
|
| 3 | 2 1 | alimdh | |- ( ph -> ( A. x ps -> A. x ch ) ) |