Description: One direction of 19.36v that can be proven without ax-6 . (Contributed by Rohan Ridenour, 16-Apr-2022) (Proof shortened by Wolf Lammen, 22-Sep-2024)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | 19.36imv | |- ( E. x ( ph -> ps ) -> ( A. x ph -> ps ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | pm2.27 | |- ( ph -> ( ( ph -> ps ) -> ps ) ) |
|
| 2 | 1 | aleximi | |- ( A. x ph -> ( E. x ( ph -> ps ) -> E. x ps ) ) |
| 3 | ax5e | |- ( E. x ps -> ps ) |
|
| 4 | 2 3 | syl6com | |- ( E. x ( ph -> ps ) -> ( A. x ph -> ps ) ) |