Theorem nfim 1446

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

Step	Hyp	Ref	Expression
1		nfim.1	. 2 ⊢ Ⅎxφ
2		nfim.2	. . 3 ⊢ Ⅎxψ
3	2	a1i 9	. 2 ⊢ (φ → Ⅎxψ)
4	1, 3	nfim1 1445	1 ⊢ Ⅎx(φ → ψ)

Syntax hints:   → wi 4  Ⅎwnf 1329

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 1316  ax-gen 1318  ax-4 1381  ax-ial 1409  ax-i5r 1410

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

This theorem is referenced by:  nfnf  1451  nfia1  1454  sb4or  1696  cbval2  1778  nfmo1  1894  mo23  1923  euexex  1967  cbvralf  2505  vtocl2gf  2592  vtocl3gf  2593  vtoclgaf  2595  vtocl2gaf  2597  vtocl3gaf  2599  rspct  2626  rspc  2627  ralab2  2682  mob  2700  csbhypf  2862  cbvralcsf  2885  dfss2f  2913  elintab  3600  nfpo  4012  nfso  4013  reusv3  4142  tfis  4233  findes  4253  dffun4f  4844  fv3  5122  tz6.12c  5128  fvmptss2  5172  fvmptssdm  5180  fvmptdf  5183  fvmptt  5187  fvmptf  5188  fmptco  5255  dff13f  5334  ovmpt2s  5547  ov2gf  5548  ovmpt2df  5555  ovi3  5560  dfoprab4f  5742  tfri3  5875  elabgft1  7024  elabgf2  7026  bj-rspgt  7032  bj-bdfindes  7171  setindis  7185  bdsetindis  7187  bj-findis  7197  bj-findes  7199