Theorem nfim 1618

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

Syntax hints:   -> wi 4   F/wnf 1506

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 1493  ax-gen 1495  ax-4 1556  ax-ial 1580  ax-i5r 1581

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

This theorem is referenced by:  nfnf  1623  nfia1  1626  sb4or  1879  cbval2  1968  nfsbv  1998  nfmo1  2089  mo23  2119  euexex  2163  nfabdw  2391  cbvralfw  2754  cbvralf  2756  vtocl2gf  2863  vtocl3gf  2864  vtoclgaf  2866  vtocl2gaf  2868  vtocl3gaf  2870  rspct  2900  rspc  2901  ralab2  2967  mob  2985  reu8nf  3110  csbhypf  3163  cbvralcsf  3187  dfss2f  3215  elintab  3934  disjiun  4078  nfpo  4392  nfso  4393  nffrfor  4439  frind  4443  nfwe  4446  reusv3  4551  tfis  4675  findes  4695  omsinds  4714  dffun4f  5334  fv3  5650  tz6.12c  5657  fvmptss2  5709  fvmptssdm  5719  fvmptdf  5722  fvmptt  5726  fvmptf  5727  fmptco  5801  dff13f  5894  ovmpos  6128  ov2gf  6129  ovmpodf  6136  ovi3  6142  dfoprab4f  6339  tfri3  6513  dom2lem  6923  findcard2  7051  findcard2s  7052  ac6sfi  7060  nfsup  7159  ismkvnex  7322  exmidfodomrlemr  7380  exmidfodomrlemrALT  7381  axpre-suploclemres  8088  uzind4s  9785  indstr  9788  supinfneg  9790  infsupneg  9791  zsupcllemstep  10449  uzsinds  10666  fimaxre2  11738  summodclem2a  11892  fsumsplitf  11919  fproddivapf  12142  fprodsplitf  12143  fprodsplit1f  12145  divalglemeunn  12432  divalglemeuneg  12434  bezoutlemmain  12519  prmind2  12642  exmidunben  12997  cnmptcom  14972  dvmptfsum  15399  lgseisenlem2  15750  gropd  15848  grstructd2dom  15849  elabgft1  16142  elabgf2  16144  bj-rspgt  16150  bj-bdfindes  16312  setindis  16330  bdsetindis  16332  bj-findis  16342  bj-findes  16344  pw1nct  16369  ismkvnnlem  16420