Theorem nfim 1586

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

Syntax hints:   -> wi 4   F/wnf 1474

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 1461  ax-gen 1463  ax-4 1524  ax-ial 1548  ax-i5r 1549

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

This theorem is referenced by:  nfnf  1591  nfia1  1594  sb4or  1847  cbval2  1936  nfsbv  1966  nfmo1  2057  mo23  2086  euexex  2130  nfabdw  2358  cbvralfw  2719  cbvralf  2721  vtocl2gf  2826  vtocl3gf  2827  vtoclgaf  2829  vtocl2gaf  2831  vtocl3gaf  2833  rspct  2861  rspc  2862  ralab2  2928  mob  2946  csbhypf  3123  cbvralcsf  3147  dfss2f  3174  elintab  3885  disjiun  4028  nfpo  4336  nfso  4337  nffrfor  4383  frind  4387  nfwe  4390  reusv3  4495  tfis  4619  findes  4639  omsinds  4658  dffun4f  5274  fv3  5581  tz6.12c  5588  fvmptss2  5636  fvmptssdm  5646  fvmptdf  5649  fvmptt  5653  fvmptf  5654  fmptco  5728  dff13f  5817  ovmpos  6046  ov2gf  6047  ovmpodf  6054  ovi3  6060  dfoprab4f  6251  tfri3  6425  dom2lem  6831  findcard2  6950  findcard2s  6951  ac6sfi  6959  nfsup  7058  ismkvnex  7221  exmidfodomrlemr  7269  exmidfodomrlemrALT  7270  axpre-suploclemres  7968  uzind4s  9664  indstr  9667  supinfneg  9669  infsupneg  9670  zsupcllemstep  10319  uzsinds  10536  fimaxre2  11392  summodclem2a  11546  fsumsplitf  11573  fproddivapf  11796  fprodsplitf  11797  fprodsplit1f  11799  divalglemeunn  12086  divalglemeuneg  12088  bezoutlemmain  12165  prmind2  12288  exmidunben  12643  cnmptcom  14534  dvmptfsum  14961  lgseisenlem2  15312  elabgft1  15424  elabgf2  15426  bj-rspgt  15432  bj-bdfindes  15595  setindis  15613  bdsetindis  15615  bj-findis  15625  bj-findes  15627  pw1nct  15647  ismkvnnlem  15696