Description: A variant of al2imi : instead of applying A. x quantifiers to the final implication, replace them with E. x . A shorter proof is possible using nfa1 , sps and eximd , but it depends on more axioms. (Contributed by Wolf Lammen, 18-Aug-2019)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | aleximi.1 | |- ( ph -> ( ps -> ch ) ) |
|
| Assertion | aleximi | |- ( A. x ph -> ( E. x ps -> E. x ch ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | aleximi.1 | |- ( ph -> ( ps -> ch ) ) |
|
| 2 | 1 | con3d | |- ( ph -> ( -. ch -> -. ps ) ) |
| 3 | 2 | al2imi | |- ( A. x ph -> ( A. x -. ch -> A. x -. ps ) ) |
| 4 | alnex | |- ( A. x -. ch <-> -. E. x ch ) |
|
| 5 | alnex | |- ( A. x -. ps <-> -. E. x ps ) |
|
| 6 | 3 4 5 | 3imtr3g | |- ( A. x ph -> ( -. E. x ch -> -. E. x ps ) ) |
| 7 | 6 | con4d | |- ( A. x ph -> ( E. x ps -> E. x ch ) ) |