Theorem nfim 1461

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 1460	1 ⊢ Ⅎx(φ → ψ)

Syntax hints:   → wi 4  Ⅎwnf 1346

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 1333  ax-gen 1335  ax-4 1397  ax-ial 1424  ax-i5r 1425

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

This theorem is referenced by:  nfnf  1466  nfia1  1469  sb4or  1711  cbval2  1793  nfmo1  1909  mo23  1938  euexex  1982  cbvralf  2521  vtocl2gf  2609  vtocl3gf  2610  vtoclgaf  2612  vtocl2gaf  2614  vtocl3gaf  2616  rspct  2643  rspc  2644  ralab2  2699  mob  2717  csbhypf  2879  cbvralcsf  2902  dfss2f  2930  elintab  3617  nfpo  4029  nfso  4030  reusv3  4158  tfis  4249  findes  4269  dffun4f  4861  fv3  5140  tz6.12c  5146  fvmptss2  5190  fvmptssdm  5198  fvmptdf  5201  fvmptt  5205  fvmptf  5206  fmptco  5273  dff13f  5352  ovmpt2s  5566  ov2gf  5567  ovmpt2df  5574  ovi3  5579  dfoprab4f  5761  tfri3  5894  dom2lem  6188  uzind4s  8309  indstr  8312  elabgft1  9252  elabgf2  9254  bj-rspgt  9260  bj-bdfindes  9409  setindis  9427  bdsetindis  9429  bj-findis  9439  bj-findes  9441