Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  nfi GIF version

Theorem nfi 1367
 Description: Deduce that 𝑥 is not free in 𝜑 from the definition. (Contributed by Mario Carneiro, 11-Aug-2016.)
Hypothesis
Ref Expression
nfi.1 (𝜑 → ∀𝑥𝜑)
Assertion
Ref Expression
nfi 𝑥𝜑

Proof of Theorem nfi
StepHypRef Expression
1 df-nf 1366 . 2 (Ⅎ𝑥𝜑 ↔ ∀𝑥(𝜑 → ∀𝑥𝜑))
2 nfi.1 . 2 (𝜑 → ∀𝑥𝜑)
31, 2mpgbir 1358 1 𝑥𝜑
 Colors of variables: wff set class Syntax hints:   → wi 4  ∀wal 1257  Ⅎwnf 1365 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-gen 1354 This theorem depends on definitions:  df-bi 114  df-nf 1366 This theorem is referenced by:  nfth  1369  nfnth  1370  nfe1  1401  nfdh  1433  nfv  1437  nfa1  1450  nfan1  1472  nfim1  1479  nfor  1482  nfal  1484  nfex  1544  nfae  1623  cbv3h  1647  nfs1  1706  nfs1v  1831  hbsb  1839  sbco2h  1854  hbsbd  1874  dvelimALT  1902  dvelimfv  1903  hbeu  1937  hbeud  1938  eu3h  1961  mo3h  1969  nfsab1  2046  nfsab  2048  nfcii  2185  nfcri  2188
 Copyright terms: Public domain W3C validator