Theorem nfim 1618

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

Syntax hints:   → wi 4  Ⅎwnf 1506

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 1493  ax-gen 1495  ax-4 1556  ax-ial 1580  ax-i5r 1581

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

This theorem is referenced by:  nfnf  1623  nfia1  1626  sb4or  1879  cbval2  1968  nfsbv  1998  nfmo1  2089  mo23  2119  euexex  2163  nfabdw  2391  cbvralfw  2754  cbvralf  2756  vtocl2gf  2863  vtocl3gf  2864  vtoclgaf  2866  vtocl2gaf  2868  vtocl3gaf  2870  rspct  2900  rspc  2901  ralab2  2967  mob  2985  reu8nf  3110  csbhypf  3163  cbvralcsf  3187  dfss2f  3215  elintab  3933  disjiun  4077  nfpo  4391  nfso  4392  nffrfor  4438  frind  4442  nfwe  4445  reusv3  4550  tfis  4674  findes  4694  omsinds  4713  dffun4f  5333  fv3  5649  tz6.12c  5656  fvmptss2  5708  fvmptssdm  5718  fvmptdf  5721  fvmptt  5725  fvmptf  5726  fmptco  5800  dff13f  5893  ovmpos  6127  ov2gf  6128  ovmpodf  6135  ovi3  6141  dfoprab4f  6337  tfri3  6511  dom2lem  6921  findcard2  7047  findcard2s  7048  ac6sfi  7056  nfsup  7155  ismkvnex  7318  exmidfodomrlemr  7376  exmidfodomrlemrALT  7377  axpre-suploclemres  8084  uzind4s  9781  indstr  9784  supinfneg  9786  infsupneg  9787  zsupcllemstep  10444  uzsinds  10661  fimaxre2  11733  summodclem2a  11887  fsumsplitf  11914  fproddivapf  12137  fprodsplitf  12138  fprodsplit1f  12140  divalglemeunn  12427  divalglemeuneg  12429  bezoutlemmain  12514  prmind2  12637  exmidunben  12992  cnmptcom  14966  dvmptfsum  15393  lgseisenlem2  15744  gropd  15842  grstructd2dom  15843  elabgft1  16100  elabgf2  16102  bj-rspgt  16108  bj-bdfindes  16270  setindis  16288  bdsetindis  16290  bj-findis  16300  bj-findes  16302  pw1nct  16328  ismkvnnlem  16379