Theorem nfim 1867

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

Syntax hints:   -> wi 4   F/wnf 1599

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-12 1803

This theorem depends on definitions:  df-bi 185  df-ex 1597  df-nf 1600

This theorem is referenced by:  nfor  1882  nfnf  1896  nfia1  1901  cbval2  2000  mo2  2287  nfmo1  2289  mo3OLD  2321  moOLD  2327  moexex  2371  moexexOLD  2372  2moOLDOLD  2384  2eu4OLD  2391  2eu6OLD  2394  cbvralf  3082  vtocl2gf  3173  vtocl3gf  3174  vtoclgaf  3176  vtocl2gaf  3178  vtocl3gaf  3180  rspct  3207  rspc  3208  ralab2  3268  mob  3285  reu2eqd  3300  csbhypf  3454  cbvralcsf  3467  dfss2f  3495  rspn0  3797  elintab  4293  axrep2  4560  axrep3  4561  reusv2lem4  4651  reusv3  4655  nfpo  4805  nffr  4853  fv3  5877  tz6.12c  5883  fvmptss  5956  fvmptdf  5959  fvmptt  5963  fvmptf  5964  fmptco  6052  dff13f  6153  ovmpt2s  6408  ov2gf  6409  ovmpt2df  6416  ov3  6421  tfis  6667  tfinds  6672  tfindes  6675  findes  6708  dfoprab4f  6839  offval22  6859  tfr3  7065  dom2lem  7552  findcard2  7756  ac6sfi  7760  dfac8clem  8409  aceq1  8494  dfac5lem5  8504  zfcndrep  8988  zfcndinf  8992  pwfseqlem4a  9035  pwfseqlem4  9036  uzindOLD  10951  uzind4s  11137  rabssnn0fi  12059  seqof2  12129  rlim2  13278  ello1mpt  13303  o1compt  13369  summolem2a  13496  sumss  13505  o1fsum  13586  prmind2  14083  mreiincl  14847  gsumcom2  16794  gsummptnn0fz  16805  gsummoncoe1  18117  mdetralt2  18878  mdetunilem2  18882  bwthOLD  19677  ptcldmpt  19850  cnmptcom  19914  elmptrab  20063  isfildlem  20093  dvmptfsum  22111  dvfsumlem2  22163  dvfsumlem4  22165  dvfsumrlim  22167  dvfsum2  22170  coeeq2  22374  dgrle  22375  rlimcnp  23023  lgseisenlem2  23353  dchrisumlema  23401  dchrisumlem2  23403  dchrisumlem3  23404  mptelee  23874  isch3  25835  atom1d  26948  mo5f  27059  ssiun2sf  27100  ssrelf  27139  fmptcof2  27174  nn0min  27279  measiun  27829  lgamgulmlem2  28212  prodmolem2a  28643  fprodn0  28686  setinds  28787  tfisg  28861  wfisg  28866  frinsg  28902  ptrest  29625  subtr  29709  subtr2  29710  fdc1  29842  ac6s6  30184  fphpd  30354  monotuz  30481  monotoddzz  30483  oddcomabszz  30484  setindtrs  30571  aomclem6  30609  flcidc  30728  fmul01  31130  fmuldfeqlem1  31132  fmuldfeq  31133  fmul01lt1lem1  31134  fmul01lt1lem2  31135  climmulf  31146  climexp  31147  climsuse  31150  climrecf  31151  climinff  31153  climaddf  31157  mullimc  31158  idlimc  31168  neglimc  31189  addlimc  31190  0ellimcdiv  31191  limclner  31193  cncfshift  31212  cncfiooicclem1  31232  iblspltprt  31291  stoweidlem3  31303  stoweidlem26  31326  stoweidlem31  31331  stoweidlem34  31334  stoweidlem42  31342  stoweidlem43  31343  stoweidlem48  31348  stoweidlem51  31351  stoweidlem59  31359  fourierdlem86  31493  fourierdlem89  31496  fourierdlem91  31498  fourierdlem112  31519  2reu4a  31661  eu2ndop1stv  31674  bnj1385  32970  bnj1468  32983  bnj110  32995  bnj849  33062  bnj900  33066  bnj981  33087  bnj1014  33097  bnj1123  33121  bnj1128  33125  bnj1384  33167  bnj1489  33191  bnj1497  33195  bj-cbval2v  33384  bj-axrep2  33456  bj-axrep3  33457  fsumshftd  33754  fsumshftdOLD  33755  cdleme31sn1  35177  cdleme32fva  35233  cdlemk36  35709