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  4039  nfpo  4348  nfso  4349  nffrfor  4395  frind  4399  nfwe  4402  reusv3  4507  tfis  4631  findes  4651  omsinds  4670  dffun4f  5287  fv3  5599  tz6.12c  5606  fvmptss2  5654  fvmptssdm  5664  fvmptdf  5667  fvmptt  5671  fvmptf  5672  fmptco  5746  dff13f  5839  ovmpos  6069  ov2gf  6070  ovmpodf  6077  ovi3  6083  dfoprab4f  6279  tfri3  6453  dom2lem  6863  findcard2  6986  findcard2s  6987  ac6sfi  6995  nfsup  7094  ismkvnex  7257  exmidfodomrlemr  7310  exmidfodomrlemrALT  7311  axpre-suploclemres  8014  uzind4s  9711  indstr  9714  supinfneg  9716  infsupneg  9717  zsupcllemstep  10372  uzsinds  10589  fimaxre2  11538  summodclem2a  11692  fsumsplitf  11719  fproddivapf  11942  fprodsplitf  11943  fprodsplit1f  11945  divalglemeunn  12232  divalglemeuneg  12234  bezoutlemmain  12319  prmind2  12442  exmidunben  12797  cnmptcom  14770  dvmptfsum  15197  lgseisenlem2  15548  gropd  15644  grstructd2dom  15645  elabgft1  15714  elabgf2  15716  bj-rspgt  15722  bj-bdfindes  15885  setindis  15903  bdsetindis  15905  bj-findis  15915  bj-findes  15917  pw1nct  15940  ismkvnnlem  15991