Theorem nfim 1625

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 1624	1 ⊢ Ⅎ𝑥(𝜑 → 𝜓)

This proof depends on syntax axioms:   → wi 4  Ⅎwnf 1513

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-4 1563  ax-ial 1587  ax-i5r 1588

This proof depends on definitions:  df-bi 117  df-nf 1514

This theorem is used by:  nfnf  1630  nfia1  1633  sb4or  1886  cbval2  1977  nfsbv  2007  nfmo1  2098  mo23  2128  euexex  2172  nfabdw  2411  cbvralfw  2775  cbvralf  2777  vtocl2gf  2885  vtocl3gf  2886  vtoclgaf  2888  vtocl2gaf  2890  vtocl3gaf  2892  rspct  2922  rspc  2923  ralab2  2990  mob  3008  reu8nf  3133  csbhypf  3186  cbvralcsf  3210  dfssf  3238  dfss2f  3239  elintab  3981  disjiun  4125  nfpo  4448  nfso  4449  nffrfor  4495  frind  4499  nfwe  4502  reusv3  4608  tfis  4732  findes  4752  omsinds  4771  dffun4f  5396  fv3  5721  tz6.12c  5728  fvmptss2  5783  fvmptssdm  5793  fvmptdf  5796  fvmptt  5800  fvmptf  5801  fmptco  5877  dff13f  5979  ovmpos  6215  ov2gf  6216  ovmpodf  6223  ovi3  6229  dfoprab4f  6431  tfri3  6642  dom2lem  7062  modom  7112  findcard2  7197  findcard2s  7198  ac6sfi  7206  nfsup  7338  ismkvnex  7501  exmidfodomrlemr  7560  exmidfodomrlemrALT  7561  axpre-suploclemres  8274  uzind4s  10006  indstr  10009  supinfneg  10011  infsupneg  10012  zsupcllemstep  10679  uzsinds  10902  fimaxre2  12016  summodclem2a  12173  fsumsplitf  12200  fproddivapf  12423  fprodsplitf  12424  fprodsplit1f  12426  divalglemeunn  12713  divalglemeuneg  12715  bezoutlemmain  12800  prmind2  12923  exmidunben  13375  gsumcom2fi  14275  cnmptcom  15524  dvmptfsum  15951  lgseisenlem2  16395  gropd  16493  grstructd2dom  16494  elabgft1  17011  elabgf2  17013  bj-rspgt  17019  bj-bdfindes  17180  setindis  17198  bdsetindis  17200  bj-findis  17210  bj-findes  17212  pw1nct  17238  ismkvnnlem  17309  nfals  17351  nfrals  17352  nfalseu  17382  nfralseu  17383