Theorem nfim 1621

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

Syntax hints:   → wi 4  Ⅎwnf 1509

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1496  ax-gen 1498  ax-4 1559  ax-ial 1583  ax-i5r 1584

This theorem depends on definitions:  df-bi 117  df-nf 1510

This theorem is referenced by:  nfnf  1626  nfia1  1629  sb4or  1882  cbval2  1971  nfsbv  2001  nfmo1  2092  mo23  2122  euexex  2166  nfabdw  2403  cbvralfw  2767  cbvralf  2769  vtocl2gf  2877  vtocl3gf  2878  vtoclgaf  2880  vtocl2gaf  2882  vtocl3gaf  2884  rspct  2914  rspc  2915  ralab2  2981  mob  2999  reu8nf  3124  csbhypf  3177  cbvralcsf  3201  dfss2f  3229  elintab  3960  disjiun  4104  nfpo  4422  nfso  4423  nffrfor  4469  frind  4473  nfwe  4476  reusv3  4581  tfis  4705  findes  4725  omsinds  4744  dffun4f  5368  fv3  5693  tz6.12c  5700  fvmptss2  5752  fvmptssdm  5762  fvmptdf  5765  fvmptt  5769  fvmptf  5770  fmptco  5843  dff13f  5943  ovmpos  6177  ov2gf  6178  ovmpodf  6185  ovi3  6191  dfoprab4f  6387  tfri3  6598  dom2lem  7011  modom  7061  findcard2  7146  findcard2s  7147  ac6sfi  7155  nfsup  7283  ismkvnex  7446  exmidfodomrlemr  7505  exmidfodomrlemrALT  7506  axpre-suploclemres  8216  uzind4s  9922  indstr  9925  supinfneg  9927  infsupneg  9928  zsupcllemstep  10589  uzsinds  10806  fimaxre2  11912  summodclem2a  12067  fsumsplitf  12094  fproddivapf  12317  fprodsplitf  12318  fprodsplit1f  12320  divalglemeunn  12607  divalglemeuneg  12609  bezoutlemmain  12694  prmind2  12817  exmidunben  13177  cnmptcom  15163  dvmptfsum  15590  lgseisenlem2  15944  gropd  16042  grstructd2dom  16043  elabgft1  16550  elabgf2  16552  bj-rspgt  16558  bj-bdfindes  16719  setindis  16737  bdsetindis  16739  bj-findis  16749  bj-findes  16751  pw1nct  16777  ismkvnnlem  16837