Theorem nfim 1625

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

This proof depends on syntax axioms:   -> wi 4   F/wnf 1513

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-4 1563  ax-ial 1587  ax-i5r 1588

This proof depends on definitions:  df-bi 117  df-nf 1514

This theorem is used by:  nfnf  1630  nfia1  1633  sb4or  1886  cbval2  1977  nfsbv  2007  nfmo1  2098  mo23  2128  euexex  2172  nfabdw  2411  cbvralfw  2775  cbvralf  2777  vtocl2gf  2885  vtocl3gf  2886  vtoclgaf  2888  vtocl2gaf  2890  vtocl3gaf  2892  rspct  2922  rspc  2923  ralab2  2990  mob  3008  reu8nf  3133  csbhypf  3186  cbvralcsf  3210  dfssf  3238  dfss2f  3239  elintab  3981  disjiun  4125  nfpo  4446  nfso  4447  nffrfor  4493  frind  4497  nfwe  4500  reusv3  4606  tfis  4730  findes  4750  omsinds  4769  dffun4f  5393  fv3  5718  tz6.12c  5725  fvmptss2  5780  fvmptssdm  5790  fvmptdf  5793  fvmptt  5797  fvmptf  5798  fmptco  5874  dff13f  5976  ovmpos  6212  ov2gf  6213  ovmpodf  6220  ovi3  6226  dfoprab4f  6427  tfri3  6638  dom2lem  7058  modom  7108  findcard2  7193  findcard2s  7194  ac6sfi  7202  nfsup  7332  ismkvnex  7495  exmidfodomrlemr  7554  exmidfodomrlemrALT  7555  axpre-suploclemres  8268  uzind4s  9999  indstr  10002  supinfneg  10004  infsupneg  10005  zsupcllemstep  10672  uzsinds  10894  fimaxre2  12008  summodclem2a  12164  fsumsplitf  12191  fproddivapf  12414  fprodsplitf  12415  fprodsplit1f  12417  divalglemeunn  12704  divalglemeuneg  12706  bezoutlemmain  12791  prmind2  12914  exmidunben  13366  cnmptcom  15448  dvmptfsum  15875  lgseisenlem2  16288  gropd  16386  grstructd2dom  16387  elabgft1  16904  elabgf2  16906  bj-rspgt  16912  bj-bdfindes  17073  setindis  17091  bdsetindis  17093  bj-findis  17103  bj-findes  17105  pw1nct  17131  ismkvnnlem  17200  nfals  17242  nfrals  17243  nfalseu  17273  nfralseu  17274