Theorem nfim 2014

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

Syntax hints:   -> wi 4   F/wnf 1678

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-10 1926  ax-12 1944

This theorem depends on definitions:  df-bi 190  df-an 377  df-ex 1675  df-nf 1679

This theorem is referenced by:  nfor  2029  nfnf  2043  nfia1  2048  cbval2  2131  mo2  2319  nfmo1  2321  moexex  2381  cbvralf  3025  vtocl2gf  3121  vtocl3gf  3122  vtoclgaf  3124  vtocl2gaf  3126  vtocl3gaf  3128  rspct  3155  rspc  3156  ralab2  3215  mob  3232  reu2eqd  3247  csbhypf  3394  cbvralcsf  3407  dfss2f  3435  rspn0  3756  elintab  4259  axrep2  4531  axrep3  4532  reusv2lem4  4621  reusv3  4625  nfpo  4779  nffr  4827  wfisg  5434  fv3  5901  tz6.12c  5907  fvmptss  5981  fvmptdf  5984  fvmptt  5988  fvmptf  5989  fmptco  6080  dff13f  6185  ovmpt2s  6447  ov2gf  6448  ovmpt2df  6455  ov3  6460  tfis  6708  tfinds  6713  tfindes  6716  findes  6750  dfoprab4f  6878  offval22  6899  tfr3  7143  dom2lem  7635  findcard2  7837  ac6sfi  7841  dfac8clem  8489  aceq1  8574  dfac5lem5  8584  zfcndrep  9065  zfcndinf  9069  pwfseqlem4a  9112  pwfseqlem4  9113  uzind4s  11248  rabssnn0fi  12230  seqof2  12303  rlim2  13609  ello1mpt  13634  o1compt  13700  summolem2a  13830  sumss  13839  o1fsum  13922  prodmolem2a  14037  fprodn0  14082  fproddivf  14090  fprodsplitf  14091  fprodsplit1f  14093  prmind2  14684  mreiincl  15551  gsumcom2  17656  gsummptnn0fz  17664  gsummoncoe1  18947  mdetralt2  19683  mdetunilem2  19687  ptcldmpt  20678  cnmptcom  20742  elmptrab  20891  isfildlem  20921  dvmptfsum  22976  dvfsumlem2  23028  dvfsumlem4  23030  dvfsumrlim  23032  dvfsum2  23035  coeeq2  23245  dgrle  23246  rlimcnp  23940  lgamgulmlem2  24004  lgseisenlem2  24327  dchrisumlema  24375  dchrisumlem2  24377  dchrisumlem3  24378  mptelee  24974  isch3  26943  atom1d  28055  vtocl2d  28158  mo5f  28169  ssiun2sf  28223  ssrelf  28270  fmptcof2  28308  aciunf1lem  28313  nn0min  28433  esum2dlem  28962  fiunelros  29045  measiun  29089  bnj1385  29693  bnj1468  29706  bnj110  29718  bnj849  29785  bnj900  29789  bnj981  29810  bnj1014  29820  bnj1123  29844  bnj1128  29848  bnj1384  29890  bnj1489  29914  bnj1497  29918  setinds  30473  tfisg  30506  frinsg  30532  subtr  31019  subtr2  31020  bj-cbval2v  31383  bj-axrep2  31449  bj-axrep3  31450  bj-mo3OLD  31492  mptsnunlem  31785  finxpreclem2  31827  finxpreclem6  31833  ptrest  31984  poimirlem24  32009  poimirlem25  32010  poimirlem26  32011  poimirlem28  32013  fdc1  32120  ac6s6  32460  fsumshftd  32568  fsumshftdOLD  32569  cdleme31sn1  33993  cdleme32fva  34049  cdlemk36  34525  fphpd  35704  monotuz  35834  monotoddzz  35836  oddcomabszz  35837  setindtrs  35925  aomclem6  35962  flcidc  36085  rababg  36224  ss2iundf  36296  binomcxplemnotnn0  36749  uzwo4  37430  fiiuncl  37444  disjf1  37495  disjinfi  37506  supxrgere  37594  supxrgelem  37598  supxrge  37599  fsumclf  37683  fsumsplitf  37684  fsummulc1f  37685  fsumnncl  37688  fsumsplit1  37689  fsumf1of  37691  fsumiunss  37692  fsumreclf  37693  fsumlessf  37694  fmul01  37696  fmuldfeqlem1  37698  fmuldfeq  37699  fmul01lt1lem1  37700  fmul01lt1lem2  37701  fprodexp  37712  fprodabs2  37713  climmulf  37720  climexp  37721  climsuse  37725  climrecf  37726  climinff  37728  climinffOLD  37729  climaddf  37733  mullimc  37734  idlimc  37744  neglimc  37766  addlimc  37767  0ellimcdiv  37768  limclner  37770  cncfshift  37789  cncfiooicclem1  37809  fprodcncf  37817  dvmptmulf  37850  dvnmptdivc  37851  dvnmul  37856  dvmptfprodlem  37857  dvmptfprod  37858  iblspltprt  37888  stoweidlem3  37901  stoweidlem26  37924  stoweidlem31  37930  stoweidlem34  37933  stoweidlem42  37941  stoweidlem43  37942  stoweidlem48  37947  stoweidlem51  37950  stoweidlem59  37958  fourierdlem86  38094  fourierdlem89  38097  fourierdlem91  38099  fourierdlem112  38120  sge0f1o  38262  sge0lempt  38290  sge0iunmptlemfi  38293  sge0iunmptlemre  38295  sge0fodjrnlem  38296  sge0iunmpt  38298  sge0ltfirpmpt2  38306  sge0isummpt2  38312  sge0xaddlem2  38314  sge0xadd  38315  meadjiun  38342  2reu4a  38648  eu2ndop1stv  38661  iunopeqop  39045  gropd  39179  grstructd  39180  2zrngmmgm  40219