Theorem nfim 1464

Description: If 𝑥 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	⊢ Ⅎ𝑥𝜑
nfim.2	⊢ Ⅎ𝑥𝜓

Assertion

Ref	Expression
nfim	⊢ Ⅎ𝑥(𝜑 → 𝜓)

Proof of Theorem nfim

Step	Hyp	Ref	Expression
1		nfim.1	. 2 ⊢ Ⅎ𝑥𝜑
2		nfim.2	. . 3 ⊢ Ⅎ𝑥𝜓
3	2	a1i 9	. 2 ⊢ (𝜑 → Ⅎ𝑥𝜓)
4	1, 3	nfim1 1463	1 ⊢ Ⅎ𝑥(𝜑 → 𝜓)

Syntax hints:   → wi 4  Ⅎwnf 1349

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1336  ax-gen 1338  ax-4 1400  ax-ial 1427  ax-i5r 1428

This theorem depends on definitions:  df-bi 110  df-nf 1350

This theorem is referenced by:  nfnf  1469  nfia1  1472  sb4or  1714  cbval2  1796  nfmo1  1912  mo23  1941  euexex  1985  cbvralf  2527  vtocl2gf  2615  vtocl3gf  2616  vtoclgaf  2618  vtocl2gaf  2620  vtocl3gaf  2622  rspct  2649  rspc  2650  ralab2  2705  mob  2723  csbhypf  2885  cbvralcsf  2908  dfss2f  2936  elintab  3626  nfpo  4038  nfso  4039  nffrfor  4085  frind  4089  nfwe  4092  reusv3  4192  tfis  4306  findes  4326  dffun4f  4918  fv3  5197  tz6.12c  5203  fvmptss2  5247  fvmptssdm  5255  fvmptdf  5258  fvmptt  5262  fvmptf  5263  fmptco  5330  dff13f  5409  ovmpt2s  5624  ov2gf  5625  ovmpt2df  5632  ovi3  5637  dfoprab4f  5819  tfri3  5953  dom2lem  6252  findcard2  6346  findcard2s  6347  ac6sfi  6352  uzind4s  8533  indstr  8536  elabgft1  9917  elabgf2  9919  bj-rspgt  9925  bj-bdfindes  10074  setindis  10092  bdsetindis  10094  bj-findis  10104  bj-findes  10106