Theorem nfim 1621

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

Syntax hints:   → wi 4  Ⅎwnf 1509

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 1496  ax-gen 1498  ax-4 1559  ax-ial 1583  ax-i5r 1584

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

This theorem is referenced by:  nfnf  1626  nfia1  1629  sb4or  1881  cbval2  1970  nfsbv  2000  nfmo1  2091  mo23  2121  euexex  2165  nfabdw  2394  cbvralfw  2757  cbvralf  2759  vtocl2gf  2867  vtocl3gf  2868  vtoclgaf  2870  vtocl2gaf  2872  vtocl3gaf  2874  rspct  2904  rspc  2905  ralab2  2971  mob  2989  reu8nf  3114  csbhypf  3167  cbvralcsf  3191  dfss2f  3219  elintab  3944  disjiun  4088  nfpo  4404  nfso  4405  nffrfor  4451  frind  4455  nfwe  4458  reusv3  4563  tfis  4687  findes  4707  omsinds  4726  dffun4f  5349  fv3  5671  tz6.12c  5678  fvmptss2  5730  fvmptssdm  5740  fvmptdf  5743  fvmptt  5747  fvmptf  5748  fmptco  5821  dff13f  5921  ovmpos  6155  ov2gf  6156  ovmpodf  6163  ovi3  6169  dfoprab4f  6365  tfri3  6576  dom2lem  6988  modom  7037  findcard2  7121  findcard2s  7122  ac6sfi  7130  nfsup  7234  ismkvnex  7397  exmidfodomrlemr  7456  exmidfodomrlemrALT  7457  axpre-suploclemres  8164  uzind4s  9868  indstr  9871  supinfneg  9873  infsupneg  9874  zsupcllemstep  10535  uzsinds  10752  fimaxre2  11850  summodclem2a  12005  fsumsplitf  12032  fproddivapf  12255  fprodsplitf  12256  fprodsplit1f  12258  divalglemeunn  12545  divalglemeuneg  12547  bezoutlemmain  12632  prmind2  12755  exmidunben  13110  cnmptcom  15092  dvmptfsum  15519  lgseisenlem2  15873  gropd  15971  grstructd2dom  15972  elabgft1  16479  elabgf2  16481  bj-rspgt  16487  bj-bdfindes  16648  setindis  16666  bdsetindis  16668  bj-findis  16678  bj-findes  16680  pw1nct  16708  ismkvnnlem  16768