Theorem nfim 1618

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

Syntax hints:   -> wi 4   F/wnf 1506

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 1493  ax-gen 1495  ax-4 1556  ax-ial 1580  ax-i5r 1581

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

This theorem is referenced by:  nfnf  1623  nfia1  1626  sb4or  1879  cbval2  1968  nfsbv  1998  nfmo1  2089  mo23  2119  euexex  2163  nfabdw  2391  cbvralfw  2754  cbvralf  2756  vtocl2gf  2863  vtocl3gf  2864  vtoclgaf  2866  vtocl2gaf  2868  vtocl3gaf  2870  rspct  2900  rspc  2901  ralab2  2967  mob  2985  reu8nf  3110  csbhypf  3163  cbvralcsf  3187  dfss2f  3215  elintab  3934  disjiun  4078  nfpo  4392  nfso  4393  nffrfor  4439  frind  4443  nfwe  4446  reusv3  4551  tfis  4675  findes  4695  omsinds  4714  dffun4f  5334  fv3  5652  tz6.12c  5659  fvmptss2  5711  fvmptssdm  5721  fvmptdf  5724  fvmptt  5728  fvmptf  5729  fmptco  5803  dff13f  5900  ovmpos  6134  ov2gf  6135  ovmpodf  6142  ovi3  6148  dfoprab4f  6345  tfri3  6519  dom2lem  6931  findcard2  7059  findcard2s  7060  ac6sfi  7068  nfsup  7170  ismkvnex  7333  exmidfodomrlemr  7391  exmidfodomrlemrALT  7392  axpre-suploclemres  8099  uzind4s  9797  indstr  9800  supinfneg  9802  infsupneg  9803  zsupcllemstep  10461  uzsinds  10678  fimaxre2  11754  summodclem2a  11908  fsumsplitf  11935  fproddivapf  12158  fprodsplitf  12159  fprodsplit1f  12161  divalglemeunn  12448  divalglemeuneg  12450  bezoutlemmain  12535  prmind2  12658  exmidunben  13013  cnmptcom  14988  dvmptfsum  15415  lgseisenlem2  15766  gropd  15864  grstructd2dom  15865  elabgft1  16225  elabgf2  16227  bj-rspgt  16233  bj-bdfindes  16395  setindis  16413  bdsetindis  16415  bj-findis  16425  bj-findes  16427  pw1nct  16456  ismkvnnlem  16508