Theorem nfim 1925

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

Syntax hints:   -> wi 4   F/wnf 1621

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-12 1859

This theorem depends on definitions:  df-bi 185  df-ex 1618  df-nf 1622

This theorem is referenced by:  nfor  1940  nfnf  1954  nfia1  1959  cbval2  2032  mo2  2295  nfmo1  2297  mo3OLD  2325  moexex  2360  2eu4OLD  2378  2eu6OLD  2381  cbvralf  3075  vtocl2gf  3166  vtocl3gf  3167  vtoclgaf  3169  vtocl2gaf  3171  vtocl3gaf  3173  rspct  3200  rspc  3201  ralab2  3261  mob  3278  reu2eqd  3293  csbhypf  3439  cbvralcsf  3452  dfss2f  3480  rspn0  3796  elintab  4282  axrep2  4552  axrep3  4553  reusv2lem4  4641  reusv3  4645  nfpo  4794  nffr  4842  fv3  5861  tz6.12c  5867  fvmptss  5940  fvmptdf  5943  fvmptt  5947  fvmptf  5948  fmptco  6040  dff13f  6142  ovmpt2s  6399  ov2gf  6400  ovmpt2df  6407  ov3  6412  tfis  6662  tfinds  6667  tfindes  6670  findes  6703  dfoprab4f  6831  offval22  6852  tfr3  7060  dom2lem  7548  findcard2  7752  ac6sfi  7756  dfac8clem  8404  aceq1  8489  dfac5lem5  8499  zfcndrep  8981  zfcndinf  8985  pwfseqlem4a  9028  pwfseqlem4  9029  uzindOLD  10953  uzind4s  11142  rabssnn0fi  12080  seqof2  12150  rlim2  13404  ello1mpt  13429  o1compt  13495  summolem2a  13622  sumss  13631  o1fsum  13712  prodmolem2a  13826  fprodn0  13868  prmind2  14315  mreiincl  15088  gsumcom2  17202  gsummptnn0fz  17212  gsummoncoe1  18544  mdetralt2  19281  mdetunilem2  19285  ptcldmpt  20284  cnmptcom  20348  elmptrab  20497  isfildlem  20527  dvmptfsum  22545  dvfsumlem2  22597  dvfsumlem4  22599  dvfsumrlim  22601  dvfsum2  22604  coeeq2  22808  dgrle  22809  rlimcnp  23496  lgseisenlem2  23826  dchrisumlema  23874  dchrisumlem2  23876  dchrisumlem3  23877  mptelee  24403  isch3  26360  atom1d  27473  mo5f  27584  ssiun2sf  27639  ssrelf  27684  fmptcof2  27727  aciunf1lem  27732  nn0min  27848  esum2dlem  28324  measiun  28429  lgamgulmlem2  28839  setinds  29453  tfisg  29527  wfisg  29532  frinsg  29568  ptrest  30291  subtr  30375  subtr2  30376  fdc1  30482  ac6s6  30823  fphpd  30992  monotuz  31119  monotoddzz  31121  oddcomabszz  31122  setindtrs  31209  aomclem6  31247  flcidc  31367  binomcxplemnotnn0  31505  fsumclf  31809  fsumsplitf  31810  fsummulc1f  31811  fsumnncl  31814  fsumsplit1  31815  fmul01  31816  fmuldfeqlem1  31818  fmuldfeq  31819  fmul01lt1lem1  31820  fmul01lt1lem2  31821  fproddivf  31830  fprodsplitf  31831  fprodsplit1f  31835  fprodexp  31842  fprodabs2  31844  climmulf  31852  climexp  31853  climsuse  31856  climrecf  31857  climinff  31859  climaddf  31863  mullimc  31864  idlimc  31874  neglimc  31895  addlimc  31896  0ellimcdiv  31897  limclner  31899  cncfshift  31918  cncfiooicclem1  31938  fprodcncf  31946  dvmptmulf  31976  dvnmptdivc  31977  dvnmul  31982  dvmptfprodlem  31983  dvmptfprod  31984  iblspltprt  32014  stoweidlem3  32027  stoweidlem26  32050  stoweidlem31  32055  stoweidlem34  32058  stoweidlem42  32066  stoweidlem43  32067  stoweidlem48  32072  stoweidlem51  32075  stoweidlem59  32083  fourierdlem86  32217  fourierdlem89  32220  fourierdlem91  32222  fourierdlem112  32243  2reu4a  32436  eu2ndop1stv  32449  2zrngmmgm  33025  bnj1385  34311  bnj1468  34324  bnj110  34336  bnj849  34403  bnj900  34407  bnj981  34428  bnj1014  34438  bnj1123  34462  bnj1128  34466  bnj1384  34508  bnj1489  34532  bnj1497  34536  bj-cbval2v  34722  bj-axrep2  34795  bj-axrep3  34796  fsumshftd  35098  fsumshftdOLD  35099  cdleme31sn1  36523  cdleme32fva  36579  cdlemk36  37055