Theorem nfim 1594

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

Syntax hints:   → wi 4  Ⅎwnf 1482

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 1469  ax-gen 1471  ax-4 1532  ax-ial 1556  ax-i5r 1557

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

This theorem is referenced by:  nfnf  1599  nfia1  1602  sb4or  1855  cbval2  1944  nfsbv  1974  nfmo1  2065  mo23  2094  euexex  2138  nfabdw  2366  cbvralfw  2727  cbvralf  2729  vtocl2gf  2834  vtocl3gf  2835  vtoclgaf  2837  vtocl2gaf  2839  vtocl3gaf  2841  rspct  2869  rspc  2870  ralab2  2936  mob  2954  csbhypf  3131  cbvralcsf  3155  dfss2f  3183  elintab  3895  disjiun  4038  nfpo  4347  nfso  4348  nffrfor  4394  frind  4398  nfwe  4401  reusv3  4506  tfis  4630  findes  4650  omsinds  4669  dffun4f  5286  fv3  5598  tz6.12c  5605  fvmptss2  5653  fvmptssdm  5663  fvmptdf  5666  fvmptt  5670  fvmptf  5671  fmptco  5745  dff13f  5838  ovmpos  6068  ov2gf  6069  ovmpodf  6076  ovi3  6082  dfoprab4f  6278  tfri3  6452  dom2lem  6862  findcard2  6985  findcard2s  6986  ac6sfi  6994  nfsup  7093  ismkvnex  7256  exmidfodomrlemr  7309  exmidfodomrlemrALT  7310  axpre-suploclemres  8013  uzind4s  9710  indstr  9713  supinfneg  9715  infsupneg  9716  zsupcllemstep  10370  uzsinds  10587  fimaxre2  11480  summodclem2a  11634  fsumsplitf  11661  fproddivapf  11884  fprodsplitf  11885  fprodsplit1f  11887  divalglemeunn  12174  divalglemeuneg  12176  bezoutlemmain  12261  prmind2  12384  exmidunben  12739  cnmptcom  14712  dvmptfsum  15139  lgseisenlem2  15490  gropd  15586  grstructd2dom  15587  elabgft1  15647  elabgf2  15649  bj-rspgt  15655  bj-bdfindes  15818  setindis  15836  bdsetindis  15838  bj-findis  15848  bj-findes  15850  pw1nct  15873  ismkvnnlem  15924