Theorem nfim 1625

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

Syntax hints:   -> wi 4   F/wnf 1513

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 1500  ax-gen 1502  ax-4 1563  ax-ial 1587  ax-i5r 1588

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

This theorem is referenced by:  nfnf  1630  nfia1  1633  sb4or  1886  cbval2  1977  nfsbv  2007  nfmo1  2098  mo23  2128  euexex  2172  nfabdw  2411  cbvralfw  2775  cbvralf  2777  vtocl2gf  2885  vtocl3gf  2886  vtoclgaf  2888  vtocl2gaf  2890  vtocl3gaf  2892  rspct  2922  rspc  2923  ralab2  2990  mob  3008  reu8nf  3133  csbhypf  3186  cbvralcsf  3210  dfssf  3238  dfss2f  3239  elintab  3976  disjiun  4120  nfpo  4441  nfso  4442  nffrfor  4488  frind  4492  nfwe  4495  reusv3  4601  tfis  4725  findes  4745  omsinds  4764  dffun4f  5388  fv3  5713  tz6.12c  5720  fvmptss2  5774  fvmptssdm  5784  fvmptdf  5787  fvmptt  5791  fvmptf  5792  fmptco  5865  dff13f  5966  ovmpos  6202  ov2gf  6203  ovmpodf  6210  ovi3  6216  dfoprab4f  6417  tfri3  6628  dom2lem  7048  modom  7098  findcard2  7183  findcard2s  7184  ac6sfi  7192  nfsup  7322  ismkvnex  7485  exmidfodomrlemr  7544  exmidfodomrlemrALT  7545  axpre-suploclemres  8258  uzind4s  9969  indstr  9972  supinfneg  9974  infsupneg  9975  zsupcllemstep  10640  uzsinds  10859  fimaxre2  11971  summodclem2a  12126  fsumsplitf  12153  fproddivapf  12376  fprodsplitf  12377  fprodsplit1f  12379  divalglemeunn  12666  divalglemeuneg  12668  bezoutlemmain  12753  prmind2  12876  exmidunben  13295  cnmptcom  15322  dvmptfsum  15749  lgseisenlem2  16104  gropd  16202  grstructd2dom  16203  elabgft1  16720  elabgf2  16722  bj-rspgt  16728  bj-bdfindes  16889  setindis  16907  bdsetindis  16909  bj-findis  16919  bj-findes  16921  pw1nct  16947  ismkvnnlem  17007