Description: Deduction form of Theorem 19.20 of Margaris p. 90, see alim . See alimdh , alimdv for variants requiring fewer axioms. (Contributed by Mario Carneiro, 24-Sep-2016)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | alimd.1 | |- F/ x ph |
|
| alimd.2 | |- ( ph -> ( ps -> ch ) ) |
||
| Assertion | alimd | |- ( ph -> ( A. x ps -> A. x ch ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | alimd.1 | |- F/ x ph |
|
| 2 | alimd.2 | |- ( ph -> ( ps -> ch ) ) |
|
| 3 | 1 | nf5ri | |- ( ph -> A. x ph ) |
| 4 | 3 2 | alimdh | |- ( ph -> ( A. x ps -> A. x ch ) ) |