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  2823  vtocl3gf  2824  vtoclgaf  2826  vtocl2gaf  2828  vtocl3gaf  2830  rspct  2858  rspc  2859  ralab2  2925  mob  2943  csbhypf  3120  cbvralcsf  3144  dfss2f  3171  elintab  3882  disjiun  4025  nfpo  4333  nfso  4334  nffrfor  4380  frind  4384  nfwe  4387  reusv3  4492  tfis  4616  findes  4636  omsinds  4655  dffun4f  5271  fv3  5578  tz6.12c  5585  fvmptss2  5633  fvmptssdm  5643  fvmptdf  5646  fvmptt  5650  fvmptf  5651  fmptco  5725  dff13f  5814  ovmpos  6043  ov2gf  6044  ovmpodf  6051  ovi3  6057  dfoprab4f  6248  tfri3  6422  dom2lem  6828  findcard2  6947  findcard2s  6948  ac6sfi  6956  nfsup  7053  ismkvnex  7216  exmidfodomrlemr  7264  exmidfodomrlemrALT  7265  axpre-suploclemres  7963  uzind4s  9658  indstr  9661  supinfneg  9663  infsupneg  9664  uzsinds  10518  fimaxre2  11373  summodclem2a  11527  fsumsplitf  11554  fproddivapf  11777  fprodsplitf  11778  fprodsplit1f  11780  divalglemeunn  12065  divalglemeuneg  12067  zsupcllemstep  12085  bezoutlemmain  12138  prmind2  12261  exmidunben  12586  cnmptcom  14477  dvmptfsum  14904  lgseisenlem2  15228  elabgft1  15340  elabgf2  15342  bj-rspgt  15348  bj-bdfindes  15511  setindis  15529  bdsetindis  15531  bj-findis  15541  bj-findes  15543  pw1nct  15563  ismkvnnlem  15612