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  5910  ovmpos  6144  ov2gf  6145  ovmpodf  6152  ovi3  6158  dfoprab4f  6355  tfri3  6532  dom2lem  6944  modom  6993  findcard2  7077  findcard2s  7078  ac6sfi  7086  nfsup  7190  ismkvnex  7353  exmidfodomrlemr  7412  exmidfodomrlemrALT  7413  axpre-suploclemres  8120  uzind4s  9823  indstr  9826  supinfneg  9828  infsupneg  9829  zsupcllemstep  10488  uzsinds  10705  fimaxre2  11787  summodclem2a  11941  fsumsplitf  11968  fproddivapf  12191  fprodsplitf  12192  fprodsplit1f  12194  divalglemeunn  12481  divalglemeuneg  12483  bezoutlemmain  12568  prmind2  12691  exmidunben  13046  cnmptcom  15021  dvmptfsum  15448  lgseisenlem2  15799  gropd  15897  grstructd2dom  15898  elabgft1  16374  elabgf2  16376  bj-rspgt  16382  bj-bdfindes  16544  setindis  16562  bdsetindis  16564  bj-findis  16574  bj-findes  16576  pw1nct  16604  ismkvnnlem  16656