Theorem nfim 1504

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

Syntax hints:   → wi 4  Ⅎwnf 1389

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1376  ax-gen 1378  ax-4 1440  ax-ial 1467  ax-i5r 1468

This theorem depends on definitions:  df-bi 115  df-nf 1390

This theorem is referenced by:  nfnf  1509  nfia1  1512  sb4or  1754  cbval2  1837  nfmo1  1953  mo23  1982  euexex  2026  cbvralf  2571  vtocl2gf  2660  vtocl3gf  2661  vtoclgaf  2663  vtocl2gaf  2665  vtocl3gaf  2667  rspct  2694  rspc  2695  ralab2  2756  mob  2774  csbhypf  2941  cbvralcsf  2964  dfss2f  2990  elintab  3647  nfpo  4056  nfso  4057  nffrfor  4103  frind  4107  nfwe  4110  reusv3  4210  tfis  4324  findes  4344  dffun4f  4938  fv3  5218  tz6.12c  5224  fvmptss2  5268  fvmptssdm  5276  fvmptdf  5279  fvmptt  5283  fvmptf  5284  fmptco  5351  dff13f  5430  ovmpt2s  5644  ov2gf  5645  ovmpt2df  5652  ovi3  5657  dfoprab4f  5839  tfri3  5976  dom2lem  6275  findcard2  6373  findcard2s  6374  ac6sfi  6379  nfsup  6405  uzind4s  8678  indstr  8681  supinfneg  8683  infsupneg  8684  uzsinds  9428  fimaxre2  10109  divalglemeunn  10321  divalglemeuneg  10323  zsupcllemstep  10341  bezoutlemmain  10387  prmind2  10502  elabgft1  10588  elabgf2  10590  bj-rspgt  10596  bj-bdfindes  10744  setindis  10762  bdsetindis  10764  bj-findis  10774  bj-findes  10776