Theorem nfim 1552

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

Syntax hints:   -> wi 4   F/wnf 1440

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 1427  ax-gen 1429  ax-4 1490  ax-ial 1514  ax-i5r 1515

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

This theorem is referenced by:  nfnf  1557  nfia1  1560  sb4or  1813  cbval2  1901  nfsbv  1927  nfmo1  2018  mo23  2047  euexex  2091  nfabdw  2318  cbvralf  2674  vtocl2gf  2774  vtocl3gf  2775  vtoclgaf  2777  vtocl2gaf  2779  vtocl3gaf  2781  rspct  2809  rspc  2810  ralab2  2876  mob  2894  csbhypf  3069  cbvralcsf  3093  dfss2f  3119  elintab  3818  disjiun  3960  nfpo  4260  nfso  4261  nffrfor  4307  frind  4311  nfwe  4314  reusv3  4418  tfis  4540  findes  4560  omsinds  4579  dffun4f  5183  fv3  5488  tz6.12c  5495  fvmptss2  5540  fvmptssdm  5549  fvmptdf  5552  fvmptt  5556  fvmptf  5557  fmptco  5630  dff13f  5715  ovmpos  5938  ov2gf  5939  ovmpodf  5946  ovi3  5951  dfoprab4f  6135  tfri3  6308  dom2lem  6710  findcard2  6827  findcard2s  6828  ac6sfi  6836  nfsup  6928  ismkvnex  7081  exmidfodomrlemr  7120  exmidfodomrlemrALT  7121  axpre-suploclemres  7804  uzind4s  9484  indstr  9487  supinfneg  9489  infsupneg  9490  uzsinds  10323  fimaxre2  11108  summodclem2a  11260  fsumsplitf  11287  fproddivapf  11510  fprodsplitf  11511  fprodsplit1f  11513  divalglemeunn  11793  divalglemeuneg  11795  zsupcllemstep  11813  bezoutlemmain  11862  prmind2  11977  exmidunben  12127  cnmptcom  12658  elabgft1  13311  elabgf2  13313  bj-rspgt  13319  bj-bdfindes  13483  setindis  13501  bdsetindis  13503  bj-findis  13513  bj-findes  13515  pw1nct  13535  ismkvnnlem  13585