Theorem nfim 1978

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 11	. 2 |- ( ph -> F/ x ps )
4	1, 3	nfim1 1977	1 |- F/ x ( ph -> ps )

Syntax hints:   -> wi 4   F/wnf 1663

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-10 1889  ax-12 1907

This theorem depends on definitions:  df-bi 188  df-ex 1660  df-nf 1664

This theorem is referenced by:  nfor  1993  nfnf  2007  nfia1  2012  cbval2  2083  mo2  2277  nfmo1  2279  moexex  2341  2eu4OLD  2359  2eu6OLD  2362  cbvralf  3056  vtocl2gf  3147  vtocl3gf  3148  vtoclgaf  3150  vtocl2gaf  3152  vtocl3gaf  3154  rspct  3181  rspc  3182  ralab2  3242  mob  3259  reu2eqd  3274  csbhypf  3420  cbvralcsf  3433  dfss2f  3461  rspn0  3780  elintab  4269  axrep2  4540  axrep3  4541  reusv2lem4  4629  reusv3  4633  nfpo  4780  nffr  4828  wfisg  5434  fv3  5894  tz6.12c  5900  fvmptss  5974  fvmptdf  5977  fvmptt  5981  fvmptf  5982  fmptco  6071  dff13f  6175  ovmpt2s  6434  ov2gf  6435  ovmpt2df  6442  ov3  6447  tfis  6695  tfinds  6700  tfindes  6703  findes  6737  dfoprab4f  6865  offval22  6886  tfr3  7125  dom2lem  7616  findcard2  7817  ac6sfi  7821  dfac8clem  8461  aceq1  8546  dfac5lem5  8556  zfcndrep  9038  zfcndinf  9042  pwfseqlem4a  9085  pwfseqlem4  9086  uzind4s  11219  rabssnn0fi  12195  seqof2  12268  rlim2  13538  ello1mpt  13563  o1compt  13629  summolem2a  13759  sumss  13768  o1fsum  13851  prodmolem2a  13966  fprodn0  14011  fproddivf  14019  fprodsplitf  14020  fprodsplit1f  14022  prmind2  14606  mreiincl  15453  gsumcom2  17542  gsummptnn0fz  17550  gsummoncoe1  18833  mdetralt2  19565  mdetunilem2  19569  ptcldmpt  20560  cnmptcom  20624  elmptrab  20773  isfildlem  20803  dvmptfsum  22804  dvfsumlem2  22856  dvfsumlem4  22858  dvfsumrlim  22860  dvfsum2  22863  coeeq2  23064  dgrle  23065  rlimcnp  23756  lgamgulmlem2  23820  lgseisenlem2  24141  dchrisumlema  24189  dchrisumlem2  24191  dchrisumlem3  24192  mptelee  24771  isch3  26729  atom1d  27841  vtocl2d  27944  mo5f  27955  ssiun2sf  28013  ssrelf  28060  fmptcof2  28099  aciunf1lem  28104  nn0min  28222  esum2dlem  28752  fiunelros  28835  measiun  28879  bnj1385  29432  bnj1468  29445  bnj110  29457  bnj849  29524  bnj900  29528  bnj981  29549  bnj1014  29559  bnj1123  29583  bnj1128  29587  bnj1384  29629  bnj1489  29653  bnj1497  29657  setinds  30211  tfisg  30244  frinsg  30270  subtr  30755  subtr2  30756  bj-cbval2v  31082  bj-axrep2  31155  bj-axrep3  31156  bj-mo3OLD  31198  mptsnunlem  31474  ptrest  31643  poimirlem24  31668  poimirlem25  31669  poimirlem26  31670  poimirlem28  31672  fdc1  31779  ac6s6  32119  fsumshftd  32232  fsumshftdOLD  32233  cdleme31sn1  33657  cdleme32fva  33713  cdlemk36  34189  fphpd  35368  monotuz  35495  monotoddzz  35497  oddcomabszz  35498  setindtrs  35586  aomclem6  35623  flcidc  35739  ss2iundf  35890  binomcxplemnotnn0  36342  uzwo4  37033  fiiuncl  37048  disjf1  37080  disjinfi  37091  supxrgere  37165  supxrgelem  37169  supxrge  37170  fsumclf  37220  fsumsplitf  37221  fsummulc1f  37222  fsumnncl  37225  fsumsplit1  37226  fsumf1of  37228  fsumiunss  37229  fmul01  37230  fmuldfeqlem1  37232  fmuldfeq  37233  fmul01lt1lem1  37234  fmul01lt1lem2  37235  fprodexp  37246  fprodabs2  37247  climmulf  37254  climexp  37255  climsuse  37259  climrecf  37260  climinff  37262  climinffOLD  37263  climaddf  37267  mullimc  37268  idlimc  37278  neglimc  37300  addlimc  37301  0ellimcdiv  37302  limclner  37304  cncfshift  37323  cncfiooicclem1  37343  fprodcncf  37351  dvmptmulf  37381  dvnmptdivc  37382  dvnmul  37387  dvmptfprodlem  37388  dvmptfprod  37389  iblspltprt  37419  stoweidlem3  37432  stoweidlem26  37455  stoweidlem31  37461  stoweidlem34  37464  stoweidlem42  37472  stoweidlem43  37473  stoweidlem48  37478  stoweidlem51  37481  stoweidlem59  37489  fourierdlem86  37624  fourierdlem89  37627  fourierdlem91  37629  fourierdlem112  37650  sge0f1o  37758  sge0lempt  37786  sge0iunmptlemfi  37789  sge0iunmptlemre  37791  sge0fodjrnlem  37792  sge0iunmpt  37794  meadjiun  37813  2reu4a  38001  eu2ndop1stv  38014  2zrngmmgm  38704