Theorem nfim 1621

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 9	. 2 |- ( ph -> F/ x ps )
4	1, 3	nfim1 1620	1 |- F/ x ( ph -> ps )

Syntax hints:   -> wi 4   F/wnf 1509

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1496  ax-gen 1498  ax-4 1559  ax-ial 1583  ax-i5r 1584

This theorem depends on definitions:  df-bi 117  df-nf 1510

This theorem is referenced by:  nfnf  1626  nfia1  1629  sb4or  1881  cbval2  1970  nfsbv  2000  nfmo1  2091  mo23  2121  euexex  2165  nfabdw  2394  cbvralfw  2757  cbvralf  2759  vtocl2gf  2867  vtocl3gf  2868  vtoclgaf  2870  vtocl2gaf  2872  vtocl3gaf  2874  rspct  2904  rspc  2905  ralab2  2971  mob  2989  reu8nf  3114  csbhypf  3167  cbvralcsf  3191  dfss2f  3219  elintab  3944  disjiun  4088  nfpo  4404  nfso  4405  nffrfor  4451  frind  4455  nfwe  4458  reusv3  4563  tfis  4687  findes  4707  omsinds  4726  dffun4f  5349  fv3  5671  tz6.12c  5678  fvmptss2  5730  fvmptssdm  5740  fvmptdf  5743  fvmptt  5747  fvmptf  5748  fmptco  5821  dff13f  5921  ovmpos  6155  ov2gf  6156  ovmpodf  6163  ovi3  6169  dfoprab4f  6365  tfri3  6576  dom2lem  6988  modom  7037  findcard2  7121  findcard2s  7122  ac6sfi  7130  nfsup  7251  ismkvnex  7414  exmidfodomrlemr  7473  exmidfodomrlemrALT  7474  axpre-suploclemres  8181  uzind4s  9885  indstr  9888  supinfneg  9890  infsupneg  9891  zsupcllemstep  10552  uzsinds  10769  fimaxre2  11867  summodclem2a  12022  fsumsplitf  12049  fproddivapf  12272  fprodsplitf  12273  fprodsplit1f  12275  divalglemeunn  12562  divalglemeuneg  12564  bezoutlemmain  12649  prmind2  12772  exmidunben  13127  cnmptcom  15109  dvmptfsum  15536  lgseisenlem2  15890  gropd  15988  grstructd2dom  15989  elabgft1  16496  elabgf2  16498  bj-rspgt  16504  bj-bdfindes  16665  setindis  16683  bdsetindis  16685  bj-findis  16695  bj-findes  16697  pw1nct  16725  ismkvnnlem  16785