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  7283  exmidfodomrlemrALT  7284  axpre-suploclemres  7987  uzind4s  9683  indstr  9686  supinfneg  9688  infsupneg  9689  zsupcllemstep  10338  uzsinds  10555  fimaxre2  11411  summodclem2a  11565  fsumsplitf  11592  fproddivapf  11815  fprodsplitf  11816  fprodsplit1f  11818  divalglemeunn  12105  divalglemeuneg  12107  bezoutlemmain  12192  prmind2  12315  exmidunben  12670  cnmptcom  14642  dvmptfsum  15069  lgseisenlem2  15420  elabgft1  15532  elabgf2  15534  bj-rspgt  15540  bj-bdfindes  15703  setindis  15721  bdsetindis  15723  bj-findis  15733  bj-findes  15735  pw1nct  15758  ismkvnnlem  15809