Metamath Proof Explorer


Theorem speimfwALT

Description: Alternate proof of speimfw (longer compressed proof, but fewer essential steps). (Contributed by NM, 23-Apr-2017) (Proof shortened by Wolf Lammen, 5-Aug-2017) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypothesis speimfw.2
|- ( x = y -> ( ph -> ps ) )
Assertion speimfwALT
|- ( -. A. x -. x = y -> ( A. x ph -> E. x ps ) )

Proof

Step Hyp Ref Expression
1 speimfw.2
 |-  ( x = y -> ( ph -> ps ) )
2 1 eximi
 |-  ( E. x x = y -> E. x ( ph -> ps ) )
3 df-ex
 |-  ( E. x x = y <-> -. A. x -. x = y )
4 19.35
 |-  ( E. x ( ph -> ps ) <-> ( A. x ph -> E. x ps ) )
5 2 3 4 3imtr3i
 |-  ( -. A. x -. x = y -> ( A. x ph -> E. x ps ) )