Theorem nfim 1596

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

Syntax hints:   -> wi 4   F/wnf 1484

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 1471  ax-gen 1473  ax-4 1534  ax-ial 1558  ax-i5r 1559

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

This theorem is referenced by:  nfnf  1601  nfia1  1604  sb4or  1857  cbval2  1946  nfsbv  1976  nfmo1  2067  mo23  2097  euexex  2141  nfabdw  2369  cbvralfw  2731  cbvralf  2733  vtocl2gf  2840  vtocl3gf  2841  vtoclgaf  2843  vtocl2gaf  2845  vtocl3gaf  2847  rspct  2877  rspc  2878  ralab2  2944  mob  2962  reu8nf  3087  csbhypf  3140  cbvralcsf  3164  dfss2f  3192  elintab  3910  disjiun  4054  nfpo  4366  nfso  4367  nffrfor  4413  frind  4417  nfwe  4420  reusv3  4525  tfis  4649  findes  4669  omsinds  4688  dffun4f  5306  fv3  5622  tz6.12c  5629  fvmptss2  5677  fvmptssdm  5687  fvmptdf  5690  fvmptt  5694  fvmptf  5695  fmptco  5769  dff13f  5862  ovmpos  6092  ov2gf  6093  ovmpodf  6100  ovi3  6106  dfoprab4f  6302  tfri3  6476  dom2lem  6886  findcard2  7012  findcard2s  7013  ac6sfi  7021  nfsup  7120  ismkvnex  7283  exmidfodomrlemr  7341  exmidfodomrlemrALT  7342  axpre-suploclemres  8049  uzind4s  9746  indstr  9749  supinfneg  9751  infsupneg  9752  zsupcllemstep  10409  uzsinds  10626  fimaxre2  11653  summodclem2a  11807  fsumsplitf  11834  fproddivapf  12057  fprodsplitf  12058  fprodsplit1f  12060  divalglemeunn  12347  divalglemeuneg  12349  bezoutlemmain  12434  prmind2  12557  exmidunben  12912  cnmptcom  14885  dvmptfsum  15312  lgseisenlem2  15663  gropd  15761  grstructd2dom  15762  elabgft1  15914  elabgf2  15916  bj-rspgt  15922  bj-bdfindes  16084  setindis  16102  bdsetindis  16104  bj-findis  16114  bj-findes  16116  pw1nct  16142  ismkvnnlem  16193