Theorem nfim 1853

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

Syntax hints:   -> wi 4   F/wnf 1589

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-12 1792

This theorem depends on definitions:  df-bi 185  df-ex 1587  df-nf 1590

This theorem is referenced by:  nfor  1868  nfnf  1875  nfia1  1880  cbval2  1975  mo2  2265  nfmo1  2267  mo3OLD  2299  moOLD  2305  moexex  2349  moexexOLD  2350  2moOLDOLD  2362  2eu4OLD  2369  2eu6OLD  2372  cbvralf  2946  vtocl2gf  3037  vtocl3gf  3038  vtoclgaf  3040  vtocl2gaf  3042  vtocl3gaf  3044  rspct  3071  rspc  3072  ralab2  3129  mob  3146  csbhypf  3312  cbvralcsf  3324  dfss2f  3352  rspn0  3654  elintab  4144  axrep2  4410  axrep3  4411  reusv2lem4  4501  reusv3  4505  nfpo  4651  nffr  4699  fv3  5708  tz6.12c  5714  fvmptss  5787  fvmptdf  5790  fvmptt  5794  fvmptf  5795  fmptco  5881  dff13f  5978  ovmpt2s  6219  ov2gf  6220  ovmpt2df  6227  ov3  6232  tfis  6470  tfinds  6475  tfindes  6478  findes  6511  dfoprab4f  6637  offval22  6657  tfr3  6863  dom2lem  7354  findcard2  7557  ac6sfi  7561  dfac8clem  8207  aceq1  8292  dfac5lem5  8302  zfcndrep  8786  zfcndinf  8790  pwfseqlem4a  8833  pwfseqlem4  8834  uzindOLD  10741  uzind4s  10919  seqof2  11869  rlim2  12979  ello1mpt  13004  o1compt  13070  summolem2a  13197  sumss  13206  o1fsum  13281  prmind2  13779  mreiincl  14539  gsumcom2  16472  mdetralt2  18420  mdetunilem2  18424  bwthOLD  19019  ptcldmpt  19192  cnmptcom  19256  elmptrab  19405  isfildlem  19435  dvmptfsum  21452  dvfsumlem2  21504  dvfsumlem4  21506  dvfsumrlim  21508  dvfsum2  21511  coeeq2  21715  dgrle  21716  rlimcnp  22364  lgseisenlem2  22694  dchrisumlema  22742  dchrisumlem2  22744  dchrisumlem3  22745  mptelee  23146  isch3  24649  atom1d  25762  mo5f  25873  ssiun2sf  25915  ssrelf  25950  fmptcof2  25984  nn0min  26095  measiun  26637  lgamgulmlem2  27021  prodmolem2a  27452  fprodn0  27495  setinds  27596  tfisg  27670  wfisg  27675  frinsg  27711  ptrest  28430  subtr  28514  subtr2  28515  fdc1  28647  ac6s6  28989  fphpd  29160  monotuz  29287  monotoddzz  29289  oddcomabszz  29290  setindtrs  29379  aomclem6  29417  flcidc  29536  fmul01  29766  fmuldfeqlem1  29768  fmuldfeq  29769  fmul01lt1lem1  29770  fmul01lt1lem2  29771  climmulf  29782  climexp  29783  climsuse  29786  climrecf  29787  climinff  29789  stoweidlem3  29803  stoweidlem26  29826  stoweidlem31  29831  stoweidlem34  29834  stoweidlem42  29842  stoweidlem43  29843  stoweidlem48  29848  stoweidlem51  29851  stoweidlem59  29859  2reu4a  30018  eu2ndop1stv  30031  rabssnn0fi  30752  gsummptnn0fz  30811  gsummoncoe1  30848  bnj1385  31831  bnj1468  31844  bnj110  31856  bnj849  31923  bnj900  31927  bnj981  31948  bnj1014  31958  bnj1123  31982  bnj1128  31986  bnj1384  32028  bnj1489  32052  bnj1497  32056  bj-cbval2v  32243  bj-axrep2  32315  bj-axrep3  32316  fsumshftd  32607  fsumshftdOLD  32608  cdleme31sn1  34030  cdleme32fva  34086  cdlemk36  34562