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  6643  dom2lem  7064  modom  7114  findcard2  7199  findcard2s  7200  ac6sfi  7208  nfsup  7338  ismkvnex  7501  exmidfodomrlemr  7560  exmidfodomrlemrALT  7561  axpre-suploclemres  8274  uzind4s  10005  indstr  10008  supinfneg  10010  infsupneg  10011  zsupcllemstep  10678  uzsinds  10901  fimaxre2  12015  summodclem2a  12172  fsumsplitf  12199  fproddivapf  12422  fprodsplitf  12423  fprodsplit1f  12425  divalglemeunn  12712  divalglemeuneg  12714  bezoutlemmain  12799  prmind2  12922  exmidunben  13374  gsumcom2fi  14274  cnmptcom  15541  dvmptfsum  15968  lgseisenlem2  16412  gropd  16510  grstructd2dom  16511  elabgft1  17028  elabgf2  17030  bj-rspgt  17036  bj-bdfindes  17197  setindis  17215  bdsetindis  17217  bj-findis  17227  bj-findes  17229  pw1nct  17255  ismkvnnlem  17326  nfals  17368  nfrals  17369  nfalseu  17399  nfralseu  17400