Theorem nfim 1625

Description: If x is not free in ph and ps, it is not free in ( ph -> ps ). (Contributed by Mario Carneiro, 11-Aug-2016.) (Proof shortened by Wolf Lammen, 2-Jan-2018.)

Hypotheses

Ref	Expression
nfim.1	|- F/ x ph
nfim.2	|- F/ x ps

Assertion

Ref	Expression
nfim	|- F/ x ( ph -> ps )

Proof of Theorem nfim

Step	Hyp	Ref	Expression
1		nfim.1	. 2 |- F/ x ph
2		nfim.2	. . 3 |- F/ x ps
3	2	a1i 9	. 2 |- ( ph -> F/ x ps )
4	1, 3	nfim1 1624	1 |- F/ x ( ph -> ps )

This proof depends on syntax axioms:   -> wi 4   F/wnf 1513

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-4 1563  ax-ial 1587  ax-i5r 1588

This proof depends on definitions:  df-bi 117  df-nf 1514

This theorem is used by:  nfnf  1630  nfia1  1633  sb4or  1886  cbval2  1977  nfsbv  2007  nfmo1  2098  mo23  2128  euexex  2172  nfabdw  2411  cbvralfw  2775  cbvralf  2777  vtocl2gf  2885  vtocl3gf  2886  vtoclgaf  2888  vtocl2gaf  2890  vtocl3gaf  2892  rspct  2922  rspc  2923  ralab2  2990  mob  3008  reu8nf  3133  csbhypf  3186  cbvralcsf  3210  dfssf  3238  dfss2f  3239  elintab  3981  disjiun  4125  nfpo  4446  nfso  4447  nffrfor  4493  frind  4497  nfwe  4500  reusv3  4606  tfis  4730  findes  4750  omsinds  4769  dffun4f  5393  fv3  5718  tz6.12c  5725  fvmptss2  5780  fvmptssdm  5790  fvmptdf  5793  fvmptt  5797  fvmptf  5798  fmptco  5874  dff13f  5976  ovmpos  6212  ov2gf  6213  ovmpodf  6220  ovi3  6226  dfoprab4f  6427  tfri3  6638  dom2lem  7058  modom  7108  findcard2  7193  findcard2s  7194  ac6sfi  7202  nfsup  7332  ismkvnex  7495  exmidfodomrlemr  7554  exmidfodomrlemrALT  7555  axpre-suploclemres  8268  uzind4s  9990  indstr  9993  supinfneg  9995  infsupneg  9996  zsupcllemstep  10662  uzsinds  10881  fimaxre2  11993  summodclem2a  12148  fsumsplitf  12175  fproddivapf  12398  fprodsplitf  12399  fprodsplit1f  12401  divalglemeunn  12688  divalglemeuneg  12690  bezoutlemmain  12775  prmind2  12898  exmidunben  13317  cnmptcom  15399  dvmptfsum  15826  lgseisenlem2  16190  gropd  16288  grstructd2dom  16289  elabgft1  16806  elabgf2  16808  bj-rspgt  16814  bj-bdfindes  16975  setindis  16993  bdsetindis  16995  bj-findis  17005  bj-findes  17007  pw1nct  17033  ismkvnnlem  17102  nfals  17144  nfrals  17145  nfalseu  17175  nfralseu  17176