Theorem nfim 1565

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

Syntax hints:   -> wi 4   F/wnf 1453

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1440  ax-gen 1442  ax-4 1503  ax-ial 1527  ax-i5r 1528

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

This theorem is referenced by:  nfnf  1570  nfia1  1573  sb4or  1826  cbval2  1914  nfsbv  1940  nfmo1  2031  mo23  2060  euexex  2104  nfabdw  2331  cbvralfw  2687  cbvralf  2689  vtocl2gf  2792  vtocl3gf  2793  vtoclgaf  2795  vtocl2gaf  2797  vtocl3gaf  2799  rspct  2827  rspc  2828  ralab2  2894  mob  2912  csbhypf  3087  cbvralcsf  3111  dfss2f  3138  elintab  3842  disjiun  3984  nfpo  4286  nfso  4287  nffrfor  4333  frind  4337  nfwe  4340  reusv3  4445  tfis  4567  findes  4587  omsinds  4606  dffun4f  5214  fv3  5519  tz6.12c  5526  fvmptss2  5571  fvmptssdm  5580  fvmptdf  5583  fvmptt  5587  fvmptf  5588  fmptco  5662  dff13f  5749  ovmpos  5976  ov2gf  5977  ovmpodf  5984  ovi3  5989  dfoprab4f  6172  tfri3  6346  dom2lem  6750  findcard2  6867  findcard2s  6868  ac6sfi  6876  nfsup  6969  ismkvnex  7131  exmidfodomrlemr  7179  exmidfodomrlemrALT  7180  axpre-suploclemres  7863  uzind4s  9549  indstr  9552  supinfneg  9554  infsupneg  9555  uzsinds  10398  fimaxre2  11190  summodclem2a  11344  fsumsplitf  11371  fproddivapf  11594  fprodsplitf  11595  fprodsplit1f  11597  divalglemeunn  11880  divalglemeuneg  11882  zsupcllemstep  11900  bezoutlemmain  11953  prmind2  12074  exmidunben  12381  cnmptcom  13092  elabgft1  13813  elabgf2  13815  bj-rspgt  13821  bj-bdfindes  13984  setindis  14002  bdsetindis  14004  bj-findis  14014  bj-findes  14016  pw1nct  14036  ismkvnnlem  14084