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  7712  uzind4s  9388  indstr  9391  supinfneg  9393  infsupneg  9394  uzsinds  10218  fimaxre2  11001  summodclem2a  11153  fsumsplitf  11180  divalglemeunn  11621  divalglemeuneg  11623  zsupcllemstep  11641  bezoutlemmain  11689  prmind2  11804  exmidunben  11942  cnmptcom  12470  elabgft1  12988  elabgf2  12990  bj-rspgt  12996  bj-bdfindes  13150  setindis  13168  bdsetindis  13170  bj-findis  13180  bj-findes  13182