Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  nfiOLD Structured version   Visualization version   GIF version

Theorem nfiOLD 1774
 Description: Obsolete proof of nf5i 2064 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
StepHypRef Expression
1 df-nfOLD 1761 . 2 (Ⅎ𝑥𝜑 ↔ ∀𝑥(𝜑 → ∀𝑥𝜑))
2 nfiOLD.1 . 2 (𝜑 → ∀𝑥𝜑)
31, 2mpgbir 1766 1 𝑥𝜑
 Colors of variables: wff setvar class Syntax hints:   → wi 4  ∀wal 1521  ℲwnfOLD 1749 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762 This theorem depends on definitions:  df-bi 197  df-nfOLD 1761 This theorem is referenced by:  nfthOLD  1775  nfnthOLD  1776  nfvOLD  1928  nfe1OLD  2073  nfdhOLD  2230  19.9hOLD  2242  nfa1OLDOLD  2243  19.21hOLD  2252  19.23hOLD  2256  exlimihOLD  2258  exlimdhOLD  2260  nfdiOLD  2261  nfim1OLD  2264  nfan1OLD  2272  hbanOLD  2276  hb3anOLD  2277
 Copyright terms: Public domain W3C validator