MPE Home 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