Theorem nfim 1596

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

Syntax hints:   → wi 4  Ⅎwnf 1484

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 1471  ax-gen 1473  ax-4 1534  ax-ial 1558  ax-i5r 1559

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

This theorem is referenced by:  nfnf  1601  nfia1  1604  sb4or  1857  cbval2  1946  nfsbv  1976  nfmo1  2067  mo23  2096  euexex  2140  nfabdw  2368  cbvralfw  2729  cbvralf  2731  vtocl2gf  2837  vtocl3gf  2838  vtoclgaf  2840  vtocl2gaf  2842  vtocl3gaf  2844  rspct  2874  rspc  2875  ralab2  2941  mob  2959  csbhypf  3136  cbvralcsf  3160  dfss2f  3188  elintab  3902  disjiun  4046  nfpo  4356  nfso  4357  nffrfor  4403  frind  4407  nfwe  4410  reusv3  4515  tfis  4639  findes  4659  omsinds  4678  dffun4f  5296  fv3  5612  tz6.12c  5619  fvmptss2  5667  fvmptssdm  5677  fvmptdf  5680  fvmptt  5684  fvmptf  5685  fmptco  5759  dff13f  5852  ovmpos  6082  ov2gf  6083  ovmpodf  6090  ovi3  6096  dfoprab4f  6292  tfri3  6466  dom2lem  6876  findcard2  7001  findcard2s  7002  ac6sfi  7010  nfsup  7109  ismkvnex  7272  exmidfodomrlemr  7326  exmidfodomrlemrALT  7327  axpre-suploclemres  8034  uzind4s  9731  indstr  9734  supinfneg  9736  infsupneg  9737  zsupcllemstep  10394  uzsinds  10611  fimaxre2  11613  summodclem2a  11767  fsumsplitf  11794  fproddivapf  12017  fprodsplitf  12018  fprodsplit1f  12020  divalglemeunn  12307  divalglemeuneg  12309  bezoutlemmain  12394  prmind2  12517  exmidunben  12872  cnmptcom  14845  dvmptfsum  15272  lgseisenlem2  15623  gropd  15721  grstructd2dom  15722  elabgft1  15853  elabgf2  15855  bj-rspgt  15861  bj-bdfindes  16023  setindis  16041  bdsetindis  16043  bj-findis  16053  bj-findes  16055  pw1nct  16081  ismkvnnlem  16132