Theorem nfim 1565

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

Syntax hints:   → wi 4  Ⅎwnf 1453

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 1440  ax-gen 1442  ax-4 1503  ax-ial 1527  ax-i5r 1528

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

This theorem is referenced by:  nfnf  1570  nfia1  1573  sb4or  1826  cbval2  1914  nfsbv  1940  nfmo1  2031  mo23  2060  euexex  2104  nfabdw  2331  cbvralfw  2687  cbvralf  2689  vtocl2gf  2792  vtocl3gf  2793  vtoclgaf  2795  vtocl2gaf  2797  vtocl3gaf  2799  rspct  2827  rspc  2828  ralab2  2894  mob  2912  csbhypf  3087  cbvralcsf  3111  dfss2f  3138  elintab  3840  disjiun  3982  nfpo  4284  nfso  4285  nffrfor  4331  frind  4335  nfwe  4338  reusv3  4443  tfis  4565  findes  4585  omsinds  4604  dffun4f  5212  fv3  5517  tz6.12c  5524  fvmptss2  5569  fvmptssdm  5578  fvmptdf  5581  fvmptt  5585  fvmptf  5586  fmptco  5659  dff13f  5746  ovmpos  5973  ov2gf  5974  ovmpodf  5981  ovi3  5986  dfoprab4f  6169  tfri3  6343  dom2lem  6746  findcard2  6863  findcard2s  6864  ac6sfi  6872  nfsup  6965  ismkvnex  7127  exmidfodomrlemr  7166  exmidfodomrlemrALT  7167  axpre-suploclemres  7850  uzind4s  9536  indstr  9539  supinfneg  9541  infsupneg  9542  uzsinds  10385  fimaxre2  11177  summodclem2a  11331  fsumsplitf  11358  fproddivapf  11581  fprodsplitf  11582  fprodsplit1f  11584  divalglemeunn  11867  divalglemeuneg  11869  zsupcllemstep  11887  bezoutlemmain  11940  prmind2  12061  exmidunben  12368  cnmptcom  13051  elabgft1  13772  elabgf2  13774  bj-rspgt  13780  bj-bdfindes  13944  setindis  13962  bdsetindis  13964  bj-findis  13974  bj-findes  13976  pw1nct  13996  ismkvnnlem  14044