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  3998  nfpo  4301  nfso  4302  nffrfor  4348  frind  4352  nfwe  4355  reusv3  4460  tfis  4582  findes  4602  omsinds  4621  dffun4f  5232  fv3  5538  tz6.12c  5545  fvmptss2  5591  fvmptssdm  5600  fvmptdf  5603  fvmptt  5607  fvmptf  5608  fmptco  5682  dff13f  5770  ovmpos  5997  ov2gf  5998  ovmpodf  6005  ovi3  6010  dfoprab4f  6193  tfri3  6367  dom2lem  6771  findcard2  6888  findcard2s  6889  ac6sfi  6897  nfsup  6990  ismkvnex  7152  exmidfodomrlemr  7200  exmidfodomrlemrALT  7201  axpre-suploclemres  7899  uzind4s  9589  indstr  9592  supinfneg  9594  infsupneg  9595  uzsinds  10441  fimaxre2  11234  summodclem2a  11388  fsumsplitf  11415  fproddivapf  11638  fprodsplitf  11639  fprodsplit1f  11641  divalglemeunn  11925  divalglemeuneg  11927  zsupcllemstep  11945  bezoutlemmain  11998  prmind2  12119  exmidunben  12426  cnmptcom  13768  lgseisenlem2  14421  elabgft1  14500  elabgf2  14502  bj-rspgt  14508  bj-bdfindes  14671  setindis  14689  bdsetindis  14691  bj-findis  14701  bj-findes  14703  pw1nct  14722  ismkvnnlem  14770