Theorem nfim 1813

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/xph
nfim.2	|- F/xps

Assertion

Ref	Expression
nfim	|- F/x(ph -> ps)

Proof of Theorem nfim

Step	Hyp	Ref	Expression
1		nfim.1	. 2 |- F/xph
2		nfim.2	. . 3 |- F/xps
3	2	a1i 10	. 2 |- (ph -> F/xps)
4	1, 3	nfim1 1811	1 |- F/x(ph -> ps)

Syntax hints:   -> wi 4   F/wnf 1544

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-11 1746

This theorem depends on definitions:  df-bi 177  df-ex 1542  df-nf 1545

This theorem is referenced by:  nfanOLD  1826  nfbiOLD  1835  nfor  1836  nfnf  1845  nfia1  1856  19.38OLD  1874  nfmo1  2215  mo  2226  moexex  2273  2mo  2282  2eu4  2287  2eu6  2289  cbvralf  2829  vtocl2gf  2916  vtocl3gf  2917  vtoclgaf  2919  vtocl2gaf  2921  vtocl3gaf  2923  rspct  2948  rspc  2949  ralab2  3001  mob  3018  csbhypf  3171  cbvralcsf  3198  dfss2f  3264  elintab  3937  fv3  5341  tz6.12c  5347  dff13f  5472  ov3  5599  fvmptss  5705  ov2gf  5711  fvmptf  5722