Theorem nfim 1594

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

Syntax hints:   → wi 4  Ⅎwnf 1482

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 1469  ax-gen 1471  ax-4 1532  ax-ial 1556  ax-i5r 1557

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

This theorem is referenced by:  nfnf  1599  nfia1  1602  sb4or  1855  cbval2  1944  nfsbv  1974  nfmo1  2065  mo23  2094  euexex  2138  nfabdw  2366  cbvralfw  2727  cbvralf  2729  vtocl2gf  2834  vtocl3gf  2835  vtoclgaf  2837  vtocl2gaf  2839  vtocl3gaf  2841  rspct  2869  rspc  2870  ralab2  2936  mob  2954  csbhypf  3131  cbvralcsf  3155  dfss2f  3183  elintab  3895  disjiun  4038  nfpo  4346  nfso  4347  nffrfor  4393  frind  4397  nfwe  4400  reusv3  4505  tfis  4629  findes  4649  omsinds  4668  dffun4f  5284  fv3  5593  tz6.12c  5600  fvmptss2  5648  fvmptssdm  5658  fvmptdf  5661  fvmptt  5665  fvmptf  5666  fmptco  5740  dff13f  5829  ovmpos  6059  ov2gf  6060  ovmpodf  6067  ovi3  6073  dfoprab4f  6269  tfri3  6443  dom2lem  6849  findcard2  6968  findcard2s  6969  ac6sfi  6977  nfsup  7076  ismkvnex  7239  exmidfodomrlemr  7292  exmidfodomrlemrALT  7293  axpre-suploclemres  7996  uzind4s  9693  indstr  9696  supinfneg  9698  infsupneg  9699  zsupcllemstep  10353  uzsinds  10570  fimaxre2  11457  summodclem2a  11611  fsumsplitf  11638  fproddivapf  11861  fprodsplitf  11862  fprodsplit1f  11864  divalglemeunn  12151  divalglemeuneg  12153  bezoutlemmain  12238  prmind2  12361  exmidunben  12716  cnmptcom  14688  dvmptfsum  15115  lgseisenlem2  15466  elabgft1  15578  elabgf2  15580  bj-rspgt  15586  bj-bdfindes  15749  setindis  15767  bdsetindis  15769  bj-findis  15779  bj-findes  15781  pw1nct  15804  ismkvnnlem  15855