Metamath Proof Explorer

Theorem nfntht

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

Ref Expression
Assertion nfntht 
|- ( -. E. x ph -> F/ x ph )

Proof

Step Hyp Ref Expression
1 pm2.21 
 |-  ( -. E. x ph -> ( E. x ph -> A. x ph ) )
2 1 nfd 
 |-  ( -. E. x ph -> F/ x ph )