Metamath Proof Explorer

Theorem nfalh

Description: Version of nfal with an 'h' hypothesis, avoiding ax-12 . (Contributed by SN, 11-Feb-2026)

Ref Expression
Hypothesis nfalh.1 
|- ( ph -> A. x ph )
Assertion nfalh 
|- F/ x A. y ph

Proof

Step Hyp Ref Expression
1 nfalh.1 
 |-  ( ph -> A. x ph )
2 1 hbal 
 |-  ( A. y ph -> A. x A. y ph )
3 2 nf5i 
 |-  F/ x A. y ph