Theorem nfiOLD 1725

Description: Obsolete proof of nf5i 2011 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	⊢ (𝜑 → ∀𝑥𝜑)

Assertion

Ref	Expression
nfiOLD	⊢ Ⅎ𝑥𝜑

Proof of Theorem nfiOLD

Step	Hyp	Ref	Expression
1		df-nfOLD 1712	. 2 ⊢ (Ⅎ𝑥𝜑 ↔ ∀𝑥(𝜑 → ∀𝑥𝜑))
2		nfiOLD.1	. 2 ⊢ (𝜑 → ∀𝑥𝜑)
3	1, 2	mpgbir 1717	1 ⊢ Ⅎ𝑥𝜑

Syntax hints:   → wi 4  ∀wal 1473  ℲwnfOLD 1700

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

This theorem depends on definitions:  df-bi 196  df-nfOLD 1712

This theorem is referenced by:  nfthOLD  1726  nfnthOLD  1727  nfvOLD  1858  nfe1OLD  2020  nfdhOLD  2182  19.9hOLD  2194  nfa1OLDOLD  2195  19.21hOLD  2204  19.23hOLD  2208  exlimihOLD  2210  exlimdhOLD  2212  nfdiOLD  2213  nfim1OLD  2216  nfan1OLD  2224  hbanOLD  2228  hb3anOLD  2229