Theorem nfim 1438

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

Syntax hints:   → wi 4  Ⅎwnf 1323

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 1310  ax-gen 1312  ax-4 1374  ax-ial 1401  ax-i5r 1402

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

This theorem is referenced by:  nfnf  1443  nfia1  1446  sb4or  1688  cbval2  1770  nfmo1  1886  mo23  1915  euexex  1959  cbvralf  2497  vtocl2gf  2584  vtocl3gf  2585  vtoclgaf  2587  vtocl2gaf  2589  vtocl3gaf  2591  rspct  2618  rspc  2619  ralab2  2674  mob  2692  csbhypf  2854  cbvralcsf  2877  dfss2f  2905  elintab  3590  nfpo  4002  nfso  4003  reusv3  4131  tfis  4222  findes  4242  dffun4f  4833  fv3  5111  tz6.12c  5117  fvmptss2  5161  fvmptssdm  5169  fvmptdf  5172  fvmptt  5176  fvmptf  5177  fmptco  5244  dff13f  5323  ovmpt2s  5536  ov2gf  5537  ovmpt2df  5544  ovi3  5549  dfoprab4f  5731  tfri3  5864  elabgft1  8254  elabgf2  8256  bj-rspgt  8262  bj-bdfindes  8405  setindis  8419  bdsetindis  8421  bj-findis  8431  bj-findes  8433