Metamath Proof Explorer


Theorem aleximi

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 ) )

Proof

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 ) )