Theorem nfim 1620

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

Syntax hints:   → wi 4  Ⅎwnf 1508

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 1495  ax-gen 1497  ax-4 1558  ax-ial 1582  ax-i5r 1583

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

This theorem is referenced by:  nfnf  1625  nfia1  1628  sb4or  1881  cbval2  1970  nfsbv  2000  nfmo1  2091  mo23  2121  euexex  2165  nfabdw  2393  cbvralfw  2756  cbvralf  2758  vtocl2gf  2866  vtocl3gf  2867  vtoclgaf  2869  vtocl2gaf  2871  vtocl3gaf  2873  rspct  2903  rspc  2904  ralab2  2970  mob  2988  reu8nf  3113  csbhypf  3166  cbvralcsf  3190  dfss2f  3218  elintab  3939  disjiun  4083  nfpo  4398  nfso  4399  nffrfor  4445  frind  4449  nfwe  4452  reusv3  4557  tfis  4681  findes  4701  omsinds  4720  dffun4f  5342  fv3  5662  tz6.12c  5669  fvmptss2  5721  fvmptssdm  5731  fvmptdf  5734  fvmptt  5738  fvmptf  5739  fmptco  5813  dff13f  5911  ovmpos  6145  ov2gf  6146  ovmpodf  6153  ovi3  6159  dfoprab4f  6356  tfri3  6533  dom2lem  6945  modom  6994  findcard2  7078  findcard2s  7079  ac6sfi  7087  nfsup  7191  ismkvnex  7354  exmidfodomrlemr  7413  exmidfodomrlemrALT  7414  axpre-suploclemres  8121  uzind4s  9824  indstr  9827  supinfneg  9829  infsupneg  9830  zsupcllemstep  10490  uzsinds  10707  fimaxre2  11792  summodclem2a  11947  fsumsplitf  11974  fproddivapf  12197  fprodsplitf  12198  fprodsplit1f  12200  divalglemeunn  12487  divalglemeuneg  12489  bezoutlemmain  12574  prmind2  12697  exmidunben  13052  cnmptcom  15028  dvmptfsum  15455  lgseisenlem2  15806  gropd  15904  grstructd2dom  15905  elabgft1  16400  elabgf2  16402  bj-rspgt  16408  bj-bdfindes  16570  setindis  16588  bdsetindis  16590  bj-findis  16600  bj-findes  16602  pw1nct  16630  ismkvnnlem  16683