Theorem nfim 1621

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

Syntax hints:   -> wi 4   F/wnf 1509

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 1496  ax-gen 1498  ax-4 1559  ax-ial 1583  ax-i5r 1584

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

This theorem is referenced by:  nfnf  1626  nfia1  1629  sb4or  1882  cbval2  1973  nfsbv  2003  nfmo1  2094  mo23  2124  euexex  2168  nfabdw  2405  cbvralfw  2769  cbvralf  2771  vtocl2gf  2879  vtocl3gf  2880  vtoclgaf  2882  vtocl2gaf  2884  vtocl3gaf  2886  rspct  2916  rspc  2917  ralab2  2984  mob  3002  reu8nf  3127  csbhypf  3180  cbvralcsf  3204  dfssf  3232  dfss2f  3233  elintab  3965  disjiun  4109  nfpo  4427  nfso  4428  nffrfor  4474  frind  4478  nfwe  4481  reusv3  4586  tfis  4710  findes  4730  omsinds  4749  dffun4f  5373  fv3  5698  tz6.12c  5705  fvmptss2  5757  fvmptssdm  5767  fvmptdf  5770  fvmptt  5774  fvmptf  5775  fmptco  5848  dff13f  5949  ovmpos  6185  ov2gf  6186  ovmpodf  6193  ovi3  6199  dfoprab4f  6400  tfri3  6611  dom2lem  7024  modom  7074  findcard2  7159  findcard2s  7160  ac6sfi  7168  nfsup  7296  ismkvnex  7459  exmidfodomrlemr  7518  exmidfodomrlemrALT  7519  axpre-suploclemres  8232  uzind4s  9940  indstr  9943  supinfneg  9945  infsupneg  9946  zsupcllemstep  10611  uzsinds  10830  fimaxre2  11937  summodclem2a  12092  fsumsplitf  12119  fproddivapf  12342  fprodsplitf  12343  fprodsplit1f  12345  divalglemeunn  12632  divalglemeuneg  12634  bezoutlemmain  12719  prmind2  12842  exmidunben  13261  cnmptcom  15289  dvmptfsum  15716  lgseisenlem2  16070  gropd  16168  grstructd2dom  16169  elabgft1  16676  elabgf2  16678  bj-rspgt  16684  bj-bdfindes  16845  setindis  16863  bdsetindis  16865  bj-findis  16875  bj-findes  16877  pw1nct  16903  ismkvnnlem  16963