Metamath Proof Explorer

Theorem nfntht2

Description: Closed form of nfnth . (Contributed by BJ, 16-Sep-2021) (Proof shortened by Wolf Lammen, 4-Sep-2022)

Ref Expression
Assertion nfntht2 
|- ( A. x -. ph -> F/ x ph )

Proof

Step Hyp Ref Expression
1 alnex 
 |-  ( A. x -. ph <-> -. E. x ph )
2 nfntht 
 |-  ( -. E. x ph -> F/ x ph )
3 1 2 sylbi 
 |-  ( A. x -. ph -> F/ x ph )