Theorem nfiOLD 1734

Description: Obsolete proof of nf5i 2024 as of 5-Oct-2021. (Contributed by Mario Carneiro, 11-Aug-2016.) (New usage is discouraged.) (Proof modification is discouraged.)

Hypothesis

Ref	Expression
nfiOLD.1	|- ( ph -> A. x ph )

Assertion

Ref	Expression
nfiOLD	|- F/ x ph

Proof of Theorem nfiOLD

Step	Hyp	Ref	Expression
1		df-nfOLD 1721	. 2 |- ( F/ x ph <-> A. x ( ph -> A. x ph ) )
2		nfiOLD.1	. 2 |- ( ph -> A. x ph )
3	1, 2	mpgbir 1726	1 |- F/ x ph

Syntax hints:   -> wi 4   A.wal 1481   F/wnfOLD 1709

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722

This theorem depends on definitions:  df-bi 197  df-nfOLD 1721

This theorem is referenced by:  nfthOLD  1735  nfnthOLD  1736  nfvOLD  1871  nfe1OLD  2033  nfdhOLD  2194  19.9hOLD  2206  nfa1OLDOLD  2207  19.21hOLD  2216  19.23hOLD  2220  exlimihOLD  2222  exlimdhOLD  2224  nfdiOLD  2225  nfim1OLD  2228  nfan1OLD  2236  hbanOLD  2240  hb3anOLD  2241