Theorem nfim 1620

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

Syntax hints:   -> wi 4   F/wnf 1508

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 1495  ax-gen 1497  ax-4 1558  ax-ial 1582  ax-i5r 1583

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

This theorem is referenced by:  nfnf  1625  nfia1  1628  sb4or  1881  cbval2  1970  nfsbv  2000  nfmo1  2091  mo23  2121  euexex  2165  nfabdw  2393  cbvralfw  2756  cbvralf  2758  vtocl2gf  2866  vtocl3gf  2867  vtoclgaf  2869  vtocl2gaf  2871  vtocl3gaf  2873  rspct  2903  rspc  2904  ralab2  2970  mob  2988  reu8nf  3113  csbhypf  3166  cbvralcsf  3190  dfss2f  3218  elintab  3939  disjiun  4083  nfpo  4398  nfso  4399  nffrfor  4445  frind  4449  nfwe  4452  reusv3  4557  tfis  4681  findes  4701  omsinds  4720  dffun4f  5342  fv3  5662  tz6.12c  5669  fvmptss2  5721  fvmptssdm  5731  fvmptdf  5734  fvmptt  5738  fvmptf  5739  fmptco  5813  dff13f  5911  ovmpos  6145  ov2gf  6146  ovmpodf  6153  ovi3  6159  dfoprab4f  6356  tfri3  6533  dom2lem  6945  modom  6994  findcard2  7078  findcard2s  7079  ac6sfi  7087  nfsup  7191  ismkvnex  7354  exmidfodomrlemr  7413  exmidfodomrlemrALT  7414  axpre-suploclemres  8121  uzind4s  9824  indstr  9827  supinfneg  9829  infsupneg  9830  zsupcllemstep  10490  uzsinds  10707  fimaxre2  11805  summodclem2a  11960  fsumsplitf  11987  fproddivapf  12210  fprodsplitf  12211  fprodsplit1f  12213  divalglemeunn  12500  divalglemeuneg  12502  bezoutlemmain  12587  prmind2  12710  exmidunben  13065  cnmptcom  15041  dvmptfsum  15468  lgseisenlem2  15819  gropd  15917  grstructd2dom  15918  elabgft1  16425  elabgf2  16427  bj-rspgt  16433  bj-bdfindes  16595  setindis  16613  bdsetindis  16615  bj-findis  16625  bj-findes  16627  pw1nct  16655  ismkvnnlem  16708