New Foundations Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  NFE Home  >  Th. List  >  nfim GIF version

Theorem nfim 1813
 Description: If x is not free in φ and ψ, it is not free in (φ → ψ). (Contributed by Mario Carneiro, 11-Aug-2016.) (Proof shortened by Wolf Lammen, 2-Jan-2018.)
Hypotheses
Ref Expression
nfim.1 xφ
nfim.2 xψ
Assertion
Ref Expression
nfim x(φψ)

Proof of Theorem nfim
StepHypRef Expression
1 nfim.1 . 2 xφ
2 nfim.2 . . 3 xψ
32a1i 10 . 2 (φ → Ⅎxψ)
41, 3nfim1 1811 1 x(φψ)
 Colors of variables: wff setvar class Syntax hints:   → wi 4  Ⅎwnf 1544 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-11 1746 This theorem depends on definitions:  df-bi 177  df-ex 1542  df-nf 1545 This theorem is referenced by:  nfanOLD  1826  nfbiOLD  1835  nfor  1836  nfnf  1845  nfia1  1856  19.38OLD  1874  nfmo1  2215  mo  2226  moexex  2273  2mo  2282  2eu4  2287  2eu6  2289  cbvralf  2829  vtocl2gf  2916  vtocl3gf  2917  vtoclgaf  2919  vtocl2gaf  2921  vtocl3gaf  2923  rspct  2948  rspc  2949  ralab2  3001  mob  3018  csbhypf  3171  cbvralcsf  3198  dfss2f  3264  elintab  3937  fv3  5341  tz6.12c  5347  dff13f  5472  ov3  5599  fvmptss  5705  ov2gf  5711  fvmptf  5722
 Copyright terms: Public domain W3C validator