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  3934  disjiun  4078  nfpo  4392  nfso  4393  nffrfor  4439  frind  4443  nfwe  4446  reusv3  4551  tfis  4675  findes  4695  omsinds  4714  dffun4f  5334  fv3  5652  tz6.12c  5659  fvmptss2  5711  fvmptssdm  5721  fvmptdf  5724  fvmptt  5728  fvmptf  5729  fmptco  5803  dff13f  5900  ovmpos  6134  ov2gf  6135  ovmpodf  6142  ovi3  6148  dfoprab4f  6345  tfri3  6519  dom2lem  6931  findcard2  7059  findcard2s  7060  ac6sfi  7068  nfsup  7170  ismkvnex  7333  exmidfodomrlemr  7391  exmidfodomrlemrALT  7392  axpre-suploclemres  8099  uzind4s  9797  indstr  9800  supinfneg  9802  infsupneg  9803  zsupcllemstep  10461  uzsinds  10678  fimaxre2  11753  summodclem2a  11907  fsumsplitf  11934  fproddivapf  12157  fprodsplitf  12158  fprodsplit1f  12160  divalglemeunn  12447  divalglemeuneg  12449  bezoutlemmain  12534  prmind2  12657  exmidunben  13012  cnmptcom  14987  dvmptfsum  15414  lgseisenlem2  15765  gropd  15863  grstructd2dom  15864  elabgft1  16197  elabgf2  16199  bj-rspgt  16205  bj-bdfindes  16367  setindis  16385  bdsetindis  16387  bj-findis  16397  bj-findes  16399  pw1nct  16428  ismkvnnlem  16480