Theorem nfim 1618

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

Syntax hints:   → wi 4  Ⅎwnf 1506

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 1493  ax-gen 1495  ax-4 1556  ax-ial 1580  ax-i5r 1581

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

This theorem is referenced by:  nfnf  1623  nfia1  1626  sb4or  1879  cbval2  1968  nfsbv  1998  nfmo1  2089  mo23  2119  euexex  2163  nfabdw  2391  cbvralfw  2754  cbvralf  2756  vtocl2gf  2864  vtocl3gf  2865  vtoclgaf  2867  vtocl2gaf  2869  vtocl3gaf  2871  rspct  2901  rspc  2902  ralab2  2968  mob  2986  reu8nf  3111  csbhypf  3164  cbvralcsf  3188  dfss2f  3216  elintab  3937  disjiun  4081  nfpo  4396  nfso  4397  nffrfor  4443  frind  4447  nfwe  4450  reusv3  4555  tfis  4679  findes  4699  omsinds  4718  dffun4f  5340  fv3  5658  tz6.12c  5665  fvmptss2  5717  fvmptssdm  5727  fvmptdf  5730  fvmptt  5734  fvmptf  5735  fmptco  5809  dff13f  5906  ovmpos  6140  ov2gf  6141  ovmpodf  6148  ovi3  6154  dfoprab4f  6351  tfri3  6528  dom2lem  6940  modom  6989  findcard2  7071  findcard2s  7072  ac6sfi  7080  nfsup  7182  ismkvnex  7345  exmidfodomrlemr  7403  exmidfodomrlemrALT  7404  axpre-suploclemres  8111  uzind4s  9814  indstr  9817  supinfneg  9819  infsupneg  9820  zsupcllemstep  10479  uzsinds  10696  fimaxre2  11778  summodclem2a  11932  fsumsplitf  11959  fproddivapf  12182  fprodsplitf  12183  fprodsplit1f  12185  divalglemeunn  12472  divalglemeuneg  12474  bezoutlemmain  12559  prmind2  12682  exmidunben  13037  cnmptcom  15012  dvmptfsum  15439  lgseisenlem2  15790  gropd  15888  grstructd2dom  15889  elabgft1  16310  elabgf2  16312  bj-rspgt  16318  bj-bdfindes  16480  setindis  16498  bdsetindis  16500  bj-findis  16510  bj-findes  16512  pw1nct  16540  ismkvnnlem  16592