Theorem nfim 1595

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 1594	1 |- F/ x ( ph -> ps )

Syntax hints:   -> wi 4   F/wnf 1483

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 1470  ax-gen 1472  ax-4 1533  ax-ial 1557  ax-i5r 1558

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

This theorem is referenced by:  nfnf  1600  nfia1  1603  sb4or  1856  cbval2  1945  nfsbv  1975  nfmo1  2066  mo23  2095  euexex  2139  nfabdw  2367  cbvralfw  2728  cbvralf  2730  vtocl2gf  2835  vtocl3gf  2836  vtoclgaf  2838  vtocl2gaf  2840  vtocl3gaf  2842  rspct  2870  rspc  2871  ralab2  2937  mob  2955  csbhypf  3132  cbvralcsf  3156  dfss2f  3184  elintab  3896  disjiun  4040  nfpo  4349  nfso  4350  nffrfor  4396  frind  4400  nfwe  4403  reusv3  4508  tfis  4632  findes  4652  omsinds  4671  dffun4f  5288  fv3  5601  tz6.12c  5608  fvmptss2  5656  fvmptssdm  5666  fvmptdf  5669  fvmptt  5673  fvmptf  5674  fmptco  5748  dff13f  5841  ovmpos  6071  ov2gf  6072  ovmpodf  6079  ovi3  6085  dfoprab4f  6281  tfri3  6455  dom2lem  6865  findcard2  6988  findcard2s  6989  ac6sfi  6997  nfsup  7096  ismkvnex  7259  exmidfodomrlemr  7312  exmidfodomrlemrALT  7313  axpre-suploclemres  8016  uzind4s  9713  indstr  9716  supinfneg  9718  infsupneg  9719  zsupcllemstep  10374  uzsinds  10591  fimaxre2  11571  summodclem2a  11725  fsumsplitf  11752  fproddivapf  11975  fprodsplitf  11976  fprodsplit1f  11978  divalglemeunn  12265  divalglemeuneg  12267  bezoutlemmain  12352  prmind2  12475  exmidunben  12830  cnmptcom  14803  dvmptfsum  15230  lgseisenlem2  15581  gropd  15677  grstructd2dom  15678  elabgft1  15751  elabgf2  15753  bj-rspgt  15759  bj-bdfindes  15922  setindis  15940  bdsetindis  15942  bj-findis  15952  bj-findes  15954  pw1nct  15977  ismkvnnlem  16028