Theorem nfim 1583

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

Syntax hints:   → wi 4  Ⅎwnf 1471

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 1458  ax-gen 1460  ax-4 1521  ax-ial 1545  ax-i5r 1546

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

This theorem is referenced by:  nfnf  1588  nfia1  1591  sb4or  1844  cbval2  1933  nfsbv  1963  nfmo1  2054  mo23  2083  euexex  2127  nfabdw  2355  cbvralfw  2716  cbvralf  2718  vtocl2gf  2822  vtocl3gf  2823  vtoclgaf  2825  vtocl2gaf  2827  vtocl3gaf  2829  rspct  2857  rspc  2858  ralab2  2924  mob  2942  csbhypf  3119  cbvralcsf  3143  dfss2f  3170  elintab  3881  disjiun  4024  nfpo  4332  nfso  4333  nffrfor  4379  frind  4383  nfwe  4386  reusv3  4491  tfis  4615  findes  4635  omsinds  4654  dffun4f  5270  fv3  5577  tz6.12c  5584  fvmptss2  5632  fvmptssdm  5642  fvmptdf  5645  fvmptt  5649  fvmptf  5650  fmptco  5724  dff13f  5813  ovmpos  6042  ov2gf  6043  ovmpodf  6050  ovi3  6055  dfoprab4f  6246  tfri3  6420  dom2lem  6826  findcard2  6945  findcard2s  6946  ac6sfi  6954  nfsup  7051  ismkvnex  7214  exmidfodomrlemr  7262  exmidfodomrlemrALT  7263  axpre-suploclemres  7961  uzind4s  9655  indstr  9658  supinfneg  9660  infsupneg  9661  uzsinds  10515  fimaxre2  11370  summodclem2a  11524  fsumsplitf  11551  fproddivapf  11774  fprodsplitf  11775  fprodsplit1f  11777  divalglemeunn  12062  divalglemeuneg  12064  zsupcllemstep  12082  bezoutlemmain  12135  prmind2  12258  exmidunben  12583  cnmptcom  14466  lgseisenlem2  15187  elabgft1  15270  elabgf2  15272  bj-rspgt  15278  bj-bdfindes  15441  setindis  15459  bdsetindis  15461  bj-findis  15471  bj-findes  15473  pw1nct  15493  ismkvnnlem  15542