Description: Inference associated with 19.36v . Version of 19.36i with a disjoint variable condition. (Contributed by NM, 5-Aug-1993) Reduce dependencies on axioms. (Revised by Wolf Lammen, 17-Jan-2020) Remove dependency on ax-6 . (Revised by Rohan Ridenour, 15-Apr-2022)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | 19.36iv.1 | |- E. x ( ph -> ps ) |
|
| Assertion | 19.36iv | |- ( A. x ph -> ps ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | 19.36iv.1 | |- E. x ( ph -> ps ) |
|
| 2 | 19.36imv | |- ( E. x ( ph -> ps ) -> ( A. x ph -> ps ) ) |
|
| 3 | 1 2 | ax-mp | |- ( A. x ph -> ps ) |