Theorem nfim 1532

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

Syntax hints:   -> wi 4   F/wnf 1417

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1404  ax-gen 1406  ax-4 1468  ax-ial 1495  ax-i5r 1496

This theorem depends on definitions:  df-bi 116  df-nf 1418

This theorem is referenced by:  nfnf  1537  nfia1  1540  sb4or  1785  cbval2  1869  nfmo1  1985  mo23  2014  euexex  2058  cbvralf  2620  vtocl2gf  2717  vtocl3gf  2718  vtoclgaf  2720  vtocl2gaf  2722  vtocl3gaf  2724  rspct  2751  rspc  2752  ralab2  2815  mob  2833  csbhypf  3002  cbvralcsf  3026  dfss2f  3052  elintab  3746  disjiun  3888  nfpo  4181  nfso  4182  nffrfor  4228  frind  4232  nfwe  4235  reusv3  4339  tfis  4455  findes  4475  omsinds  4493  dffun4f  5095  fv3  5396  tz6.12c  5403  fvmptss2  5448  fvmptssdm  5457  fvmptdf  5460  fvmptt  5464  fvmptf  5465  fmptco  5538  dff13f  5623  ovmpos  5846  ov2gf  5847  ovmpodf  5854  ovi3  5859  dfoprab4f  6043  tfri3  6216  dom2lem  6618  findcard2  6734  findcard2s  6735  ac6sfi  6743  nfsup  6829  exmidfodomrlemr  7003  exmidfodomrlemrALT  7004  uzind4s  9281  indstr  9284  supinfneg  9286  infsupneg  9287  uzsinds  10102  fimaxre2  10884  summodclem2a  11036  fsumsplitf  11063  divalglemeunn  11460  divalglemeuneg  11462  zsupcllemstep  11480  bezoutlemmain  11526  prmind2  11641  exmidunben  11778  cnmptcom  12303  elabgft1  12668  elabgf2  12670  bj-rspgt  12676  bj-bdfindes  12830  setindis  12848  bdsetindis  12850  bj-findis  12860  bj-findes  12862