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  2830  vtocl2gf  2917  vtocl3gf  2918  vtoclgaf  2920  vtocl2gaf  2922  vtocl3gaf  2924  rspct  2949  rspc  2950  ralab2  3002  mob  3019  csbhypf  3172  cbvralcsf  3199  dfss2f  3265  elintab  3938  fv3  5342  tz6.12c  5348  dff13f  5473  ov3  5600  fvmptss  5706  ov2gf  5712  fvmptf  5723