Theorem nfim 1586

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

Syntax hints:   → wi 4  Ⅎwnf 1474

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 1461  ax-gen 1463  ax-4 1524  ax-ial 1548  ax-i5r 1549

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

This theorem is referenced by:  nfnf  1591  nfia1  1594  sb4or  1847  cbval2  1936  nfsbv  1966  nfmo1  2057  mo23  2086  euexex  2130  nfabdw  2358  cbvralfw  2719  cbvralf  2721  vtocl2gf  2826  vtocl3gf  2827  vtoclgaf  2829  vtocl2gaf  2831  vtocl3gaf  2833  rspct  2861  rspc  2862  ralab2  2928  mob  2946  csbhypf  3123  cbvralcsf  3147  dfss2f  3175  elintab  3886  disjiun  4029  nfpo  4337  nfso  4338  nffrfor  4384  frind  4388  nfwe  4391  reusv3  4496  tfis  4620  findes  4640  omsinds  4659  dffun4f  5275  fv3  5584  tz6.12c  5591  fvmptss2  5639  fvmptssdm  5649  fvmptdf  5652  fvmptt  5656  fvmptf  5657  fmptco  5731  dff13f  5820  ovmpos  6050  ov2gf  6051  ovmpodf  6058  ovi3  6064  dfoprab4f  6260  tfri3  6434  dom2lem  6840  findcard2  6959  findcard2s  6960  ac6sfi  6968  nfsup  7067  ismkvnex  7230  exmidfodomrlemr  7281  exmidfodomrlemrALT  7282  axpre-suploclemres  7985  uzind4s  9681  indstr  9684  supinfneg  9686  infsupneg  9687  zsupcllemstep  10336  uzsinds  10553  fimaxre2  11409  summodclem2a  11563  fsumsplitf  11590  fproddivapf  11813  fprodsplitf  11814  fprodsplit1f  11816  divalglemeunn  12103  divalglemeuneg  12105  bezoutlemmain  12190  prmind2  12313  exmidunben  12668  cnmptcom  14618  dvmptfsum  15045  lgseisenlem2  15396  elabgft1  15508  elabgf2  15510  bj-rspgt  15516  bj-bdfindes  15679  setindis  15697  bdsetindis  15699  bj-findis  15709  bj-findes  15711  pw1nct  15734  ismkvnnlem  15783