Metamath Proof Explorer

Theorem 19.9ht

Description: A closed version of 19.9h . (Contributed by NM, 13-May-1993) (Proof shortened by Wolf Lammen, 3-Mar-2018)

Ref Expression
Assertion 19.9ht 
|- ( A. x ( ph -> A. x ph ) -> ( E. x ph -> ph ) )

Proof

Step Hyp Ref Expression
1 nf5-1 
 |-  ( A. x ( ph -> A. x ph ) -> F/ x ph )
2 1 19.9d 
 |-  ( A. x ( ph -> A. x ph ) -> ( E. x ph -> ph ) )