Theorem nfim 1857

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

Syntax hints:   -> wi 4   F/wnf 1594

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1713  ax-7 1733  ax-10 1780  ax-12 1797

This theorem depends on definitions:  df-bi 185  df-ex 1592  df-nf 1595

This theorem is referenced by:  nfor  1872  nfnf  1879  nfia1  1884  cbval2  1980  mo2  2268  nfmo1  2270  mo3OLD  2302  moOLD  2308  moexex  2352  moexexOLD  2353  2mo  2362  2moOLD  2363  2eu4OLD  2369  2eu6  2371  cbvralf  2939  vtocl2gf  3029  vtocl3gf  3030  vtoclgaf  3032  vtocl2gaf  3034  vtocl3gaf  3036  rspct  3063  rspc  3064  ralab2  3121  mob  3138  csbhypf  3304  cbvralcsf  3316  dfss2f  3344  rspn0  3646  elintab  4136  axrep2  4402  axrep3  4403  reusv2lem4  4493  reusv3  4497  nfpo  4642  nffr  4690  fv3  5700  tz6.12c  5706  fvmptss  5779  fvmptdf  5782  fvmptt  5786  fvmptf  5787  fmptco  5873  dff13f  5970  ovmpt2s  6213  ov2gf  6214  ovmpt2df  6221  ov3  6226  tfis  6464  tfinds  6469  tfindes  6472  findes  6505  dfoprab4f  6631  offval22  6651  tfr3  6854  dom2lem  7345  findcard2  7548  ac6sfi  7552  dfac8clem  8198  aceq1  8283  dfac5lem5  8293  zfcndrep  8777  zfcndinf  8781  pwfseqlem4a  8824  pwfseqlem4  8825  uzindOLD  10732  uzind4s  10910  seqof2  11860  rlim2  12970  ello1mpt  12995  o1compt  13061  summolem2a  13188  sumss  13197  o1fsum  13272  prmind2  13770  mreiincl  14530  gsumcom2  16457  mdetralt2  18374  mdetunilem2  18378  bwthOLD  18973  ptcldmpt  19146  cnmptcom  19210  elmptrab  19359  isfildlem  19389  dvmptfsum  21406  dvfsumlem2  21458  dvfsumlem4  21460  dvfsumrlim  21462  dvfsum2  21465  coeeq2  21669  dgrle  21670  rlimcnp  22318  lgseisenlem2  22648  dchrisumlema  22696  dchrisumlem2  22698  dchrisumlem3  22699  mptelee  23076  isch3  24579  atom1d  25692  mo5f  25803  ssiun2sf  25845  ssrelf  25880  fmptcof2  25914  nn0min  26023  measiun  26568  lgamgulmlem2  26946  prodmolem2a  27376  fprodn0  27419  setinds  27520  tfisg  27594  wfisg  27599  frinsg  27635  ptrest  28350  subtr  28434  subtr2  28435  fdc1  28567  ac6s6  28909  fphpd  29080  monotuz  29207  monotoddzz  29209  oddcomabszz  29210  setindtrs  29299  aomclem6  29337  flcidc  29456  fmul01  29686  fmuldfeqlem1  29688  fmuldfeq  29689  fmul01lt1lem1  29690  fmul01lt1lem2  29691  climmulf  29702  climexp  29703  climsuse  29706  climrecf  29707  climinff  29709  stoweidlem3  29723  stoweidlem26  29746  stoweidlem31  29751  stoweidlem34  29754  stoweidlem42  29762  stoweidlem43  29763  stoweidlem48  29768  stoweidlem51  29771  stoweidlem59  29779  2reu4a  29938  eu2ndop1stv  29951  bnj1385  31660  bnj1468  31673  bnj110  31685  bnj849  31752  bnj900  31756  bnj981  31777  bnj1014  31787  bnj1123  31811  bnj1128  31815  bnj1384  31857  bnj1489  31881  bnj1497  31885  bj-cbval2v  32001  bj-axrep2  32070  bj-axrep3  32071  cdleme31sn1  33747  cdleme32fva  33803  cdlemk36  34279