Theorem nfim 1572

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

Syntax hints:   -> wi 4   F/wnf 1460

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 1447  ax-gen 1449  ax-4 1510  ax-ial 1534  ax-i5r 1535

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

This theorem is referenced by:  nfnf  1577  nfia1  1580  sb4or  1833  cbval2  1921  nfsbv  1947  nfmo1  2038  mo23  2067  euexex  2111  nfabdw  2338  cbvralfw  2694  cbvralf  2696  vtocl2gf  2799  vtocl3gf  2800  vtoclgaf  2802  vtocl2gaf  2804  vtocl3gaf  2806  rspct  2834  rspc  2835  ralab2  2901  mob  2919  csbhypf  3095  cbvralcsf  3119  dfss2f  3146  elintab  3855  disjiun  3997  nfpo  4300  nfso  4301  nffrfor  4347  frind  4351  nfwe  4354  reusv3  4459  tfis  4581  findes  4601  omsinds  4620  dffun4f  5231  fv3  5537  tz6.12c  5544  fvmptss2  5590  fvmptssdm  5599  fvmptdf  5602  fvmptt  5606  fvmptf  5607  fmptco  5681  dff13f  5768  ovmpos  5995  ov2gf  5996  ovmpodf  6003  ovi3  6008  dfoprab4f  6191  tfri3  6365  dom2lem  6769  findcard2  6886  findcard2s  6887  ac6sfi  6895  nfsup  6988  ismkvnex  7150  exmidfodomrlemr  7198  exmidfodomrlemrALT  7199  axpre-suploclemres  7897  uzind4s  9586  indstr  9589  supinfneg  9591  infsupneg  9592  uzsinds  10437  fimaxre2  11228  summodclem2a  11382  fsumsplitf  11409  fproddivapf  11632  fprodsplitf  11633  fprodsplit1f  11635  divalglemeunn  11918  divalglemeuneg  11920  zsupcllemstep  11938  bezoutlemmain  11991  prmind2  12112  exmidunben  12419  cnmptcom  13669  elabgft1  14390  elabgf2  14392  bj-rspgt  14398  bj-bdfindes  14561  setindis  14579  bdsetindis  14581  bj-findis  14591  bj-findes  14593  pw1nct  14612  ismkvnnlem  14660