Theorem nfim 1560

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

Syntax hints:   -> wi 4   F/wnf 1448

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1435  ax-gen 1437  ax-4 1498  ax-ial 1522  ax-i5r 1523

This theorem depends on definitions:  df-bi 116  df-nf 1449

This theorem is referenced by:  nfnf  1565  nfia1  1568  sb4or  1821  cbval2  1909  nfsbv  1935  nfmo1  2026  mo23  2055  euexex  2099  nfabdw  2327  cbvralfw  2683  cbvralf  2685  vtocl2gf  2788  vtocl3gf  2789  vtoclgaf  2791  vtocl2gaf  2793  vtocl3gaf  2795  rspct  2823  rspc  2824  ralab2  2890  mob  2908  csbhypf  3083  cbvralcsf  3107  dfss2f  3133  elintab  3835  disjiun  3977  nfpo  4279  nfso  4280  nffrfor  4326  frind  4330  nfwe  4333  reusv3  4438  tfis  4560  findes  4580  omsinds  4599  dffun4f  5204  fv3  5509  tz6.12c  5516  fvmptss2  5561  fvmptssdm  5570  fvmptdf  5573  fvmptt  5577  fvmptf  5578  fmptco  5651  dff13f  5738  ovmpos  5965  ov2gf  5966  ovmpodf  5973  ovi3  5978  dfoprab4f  6161  tfri3  6335  dom2lem  6738  findcard2  6855  findcard2s  6856  ac6sfi  6864  nfsup  6957  ismkvnex  7119  exmidfodomrlemr  7158  exmidfodomrlemrALT  7159  axpre-suploclemres  7842  uzind4s  9528  indstr  9531  supinfneg  9533  infsupneg  9534  uzsinds  10377  fimaxre2  11168  summodclem2a  11322  fsumsplitf  11349  fproddivapf  11572  fprodsplitf  11573  fprodsplit1f  11575  divalglemeunn  11858  divalglemeuneg  11860  zsupcllemstep  11878  bezoutlemmain  11931  prmind2  12052  exmidunben  12359  cnmptcom  12938  elabgft1  13659  elabgf2  13661  bj-rspgt  13667  bj-bdfindes  13831  setindis  13849  bdsetindis  13851  bj-findis  13861  bj-findes  13863  pw1nct  13883  ismkvnnlem  13931