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  2695  cbvralf  2697  vtocl2gf  2800  vtocl3gf  2801  vtoclgaf  2803  vtocl2gaf  2805  vtocl3gaf  2807  rspct  2835  rspc  2836  ralab2  2902  mob  2920  csbhypf  3096  cbvralcsf  3120  dfss2f  3147  elintab  3856  disjiun  3999  nfpo  4302  nfso  4303  nffrfor  4349  frind  4353  nfwe  4356  reusv3  4461  tfis  4583  findes  4603  omsinds  4622  dffun4f  5233  fv3  5539  tz6.12c  5546  fvmptss2  5592  fvmptssdm  5601  fvmptdf  5604  fvmptt  5608  fvmptf  5609  fmptco  5683  dff13f  5771  ovmpos  5998  ov2gf  5999  ovmpodf  6006  ovi3  6011  dfoprab4f  6194  tfri3  6368  dom2lem  6772  findcard2  6889  findcard2s  6890  ac6sfi  6898  nfsup  6991  ismkvnex  7153  exmidfodomrlemr  7201  exmidfodomrlemrALT  7202  axpre-suploclemres  7900  uzind4s  9590  indstr  9593  supinfneg  9595  infsupneg  9596  uzsinds  10442  fimaxre2  11235  summodclem2a  11389  fsumsplitf  11416  fproddivapf  11639  fprodsplitf  11640  fprodsplit1f  11642  divalglemeunn  11926  divalglemeuneg  11928  zsupcllemstep  11946  bezoutlemmain  11999  prmind2  12120  exmidunben  12427  cnmptcom  13801  lgseisenlem2  14454  elabgft1  14533  elabgf2  14535  bj-rspgt  14541  bj-bdfindes  14704  setindis  14722  bdsetindis  14724  bj-findis  14734  bj-findes  14736  pw1nct  14755  ismkvnnlem  14803