Theorem nfim 1551

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

Syntax hints:   → wi 4  Ⅎwnf 1436

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1423  ax-gen 1425  ax-4 1487  ax-ial 1514  ax-i5r 1515

This theorem depends on definitions:  df-bi 116  df-nf 1437

This theorem is referenced by:  nfnf  1556  nfia1  1559  sb4or  1805  cbval2  1891  nfmo1  2009  mo23  2038  euexex  2082  cbvralf  2646  vtocl2gf  2743  vtocl3gf  2744  vtoclgaf  2746  vtocl2gaf  2748  vtocl3gaf  2750  rspct  2777  rspc  2778  ralab2  2843  mob  2861  csbhypf  3033  cbvralcsf  3057  dfss2f  3083  elintab  3777  disjiun  3919  nfpo  4218  nfso  4219  nffrfor  4265  frind  4269  nfwe  4272  reusv3  4376  tfis  4492  findes  4512  omsinds  4530  dffun4f  5134  fv3  5437  tz6.12c  5444  fvmptss2  5489  fvmptssdm  5498  fvmptdf  5501  fvmptt  5505  fvmptf  5506  fmptco  5579  dff13f  5664  ovmpos  5887  ov2gf  5888  ovmpodf  5895  ovi3  5900  dfoprab4f  6084  tfri3  6257  dom2lem  6659  findcard2  6776  findcard2s  6777  ac6sfi  6785  nfsup  6872  ismkvnex  7022  exmidfodomrlemr  7051  exmidfodomrlemrALT  7052  axpre-suploclemres  7702  uzind4s  9378  indstr  9381  supinfneg  9383  infsupneg  9384  uzsinds  10208  fimaxre2  10991  summodclem2a  11143  fsumsplitf  11170  divalglemeunn  11607  divalglemeuneg  11609  zsupcllemstep  11627  bezoutlemmain  11675  prmind2  11790  exmidunben  11928  cnmptcom  12456  elabgft1  12974  elabgf2  12976  bj-rspgt  12982  bj-bdfindes  13136  setindis  13154  bdsetindis  13156  bj-findis  13166  bj-findes  13168