Theorem nfim 1551

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

Syntax hints:   -> wi 4   F/wnf 1436

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1423  ax-gen 1425  ax-4 1487  ax-ial 1514  ax-i5r 1515

This theorem depends on definitions:  df-bi 116  df-nf 1437

This theorem is referenced by:  nfnf  1556  nfia1  1559  sb4or  1805  cbval2  1893  nfmo1  2011  mo23  2040  euexex  2084  cbvralf  2648  vtocl2gf  2748  vtocl3gf  2749  vtoclgaf  2751  vtocl2gaf  2753  vtocl3gaf  2755  rspct  2782  rspc  2783  ralab2  2848  mob  2866  csbhypf  3038  cbvralcsf  3062  dfss2f  3088  elintab  3782  disjiun  3924  nfpo  4223  nfso  4224  nffrfor  4270  frind  4274  nfwe  4277  reusv3  4381  tfis  4497  findes  4517  omsinds  4535  dffun4f  5139  fv3  5444  tz6.12c  5451  fvmptss2  5496  fvmptssdm  5505  fvmptdf  5508  fvmptt  5512  fvmptf  5513  fmptco  5586  dff13f  5671  ovmpos  5894  ov2gf  5895  ovmpodf  5902  ovi3  5907  dfoprab4f  6091  tfri3  6264  dom2lem  6666  findcard2  6783  findcard2s  6784  ac6sfi  6792  nfsup  6879  ismkvnex  7029  exmidfodomrlemr  7058  exmidfodomrlemrALT  7059  axpre-suploclemres  7709  uzind4s  9385  indstr  9388  supinfneg  9390  infsupneg  9391  uzsinds  10215  fimaxre2  10998  summodclem2a  11150  fsumsplitf  11177  divalglemeunn  11618  divalglemeuneg  11620  zsupcllemstep  11638  bezoutlemmain  11686  prmind2  11801  exmidunben  11939  cnmptcom  12467  elabgft1  12985  elabgf2  12987  bj-rspgt  12993  bj-bdfindes  13147  setindis  13165  bdsetindis  13167  bj-findis  13177  bj-findes  13179