Theorem nfim 1828

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

Syntax hints:   -> wi 4   F/wnf 1550

This theorem is referenced by:  nfanOLD  1844  nfbiOLD  1853  nfor  1854  nfnf  1863  nfia1  1871  19.38OLD  1891  nfmo1  2265  mo  2276  moexex  2323  2mo  2332  2eu4  2337  2eu6  2339  cbvralf  2886  vtocl2gf  2973  vtocl3gf  2974  vtoclgaf  2976  vtocl2gaf  2978  vtocl3gaf  2980  rspct  3005  rspc  3006  ralab2  3059  mob  3076  csbhypf  3246  cbvralcsf  3271  dfss2f  3299  elintab  4021  axrep2  4282  axrep3  4283  nfpo  4468  nffr  4516  reusv2lem4  4686  reusv3  4690  tfis  4793  tfinds  4798  tfindes  4801  findes  4834  fv3  5703  tz6.12c  5709  fvmptss  5772  fvmptdf  5775  fvmptt  5779  fvmptf  5780  fmptco  5860  dff13f  5965  ovmpt2s  6156  ov2gf  6157  ovmpt2df  6164  ov3  6169  dfoprab4f  6364  tfr3  6619  dom2lem  7106  findcard2  7307  ac6sfi  7310  dfac8clem  7869  aceq1  7954  dfac5lem5  7964  zfcndrep  8445  zfcndinf  8449  pwfseqlem4a  8492  pwfseqlem4  8493  uzindOLD  10320  uzind4s  10492  seqof2  11336  rlim2  12245  ello1mpt  12270  o1compt  12336  summolem2a  12464  sumss  12473  o1fsum  12547  prmind2  13045  mreiincl  13776  gsumcom2  15504  ptcldmpt  17599  cnmptcom  17663  elmptrab  17812  isfildlem  17842  dvmptfsum  19812  dvfsumlem2  19864  dvfsumlem4  19866  dvfsumrlim  19868  dvfsum2  19871  coeeq2  20114  dgrle  20115  rlimcnp  20757  lgseisenlem2  21087  dchrisumlema  21135  dchrisumlem2  21137  dchrisumlem3  21138  isch3  22697  atom1d  23809  mo5f  23925  ssiun2sf  23963  fmptcof2  24029  measiun  24525  lgamgulmlem2  24767  prodmolem2a  25213  fprodn0  25256  setinds  25348  tfisg  25418  wfisg  25423  frinsg  25459  mptelee  25738  subtr  26207  subtr2  26208  fdc1  26340  fphpd  26767  monotuz  26894  monotoddzz  26896  oddcomabszz  26897  setindtrs  26986  aomclem6  27024  flcidc  27247  fmul01  27577  fmuldfeqlem1  27579  fmuldfeq  27580  fmul01lt1lem1  27581  fmul01lt1lem2  27582  climmulf  27597  climexp  27598  climsuse  27601  climrecf  27602  climinff  27604  stoweidlem3  27619  stoweidlem26  27642  stoweidlem31  27647  stoweidlem34  27650  stoweidlem42  27658  stoweidlem43  27659  stoweidlem48  27664  stoweidlem51  27667  stoweidlem59  27675  2reu4a  27834  eu2ndop1stv  27847  bnj1385  28910  bnj1468  28923  bnj110  28935  bnj849  29002  bnj900  29006  bnj981  29027  bnj1014  29037  bnj1123  29061  bnj1128  29065  bnj1384  29107  bnj1489  29131  bnj1497  29135  cdleme31sn1  30863  cdleme32fva  30919  cdlemk36  31395

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-11 1757

This theorem depends on definitions:  df-bi 178  df-ex 1548  df-nf 1551