MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  nfim Structured version   Unicode version

Theorem nfim 1833
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
StepHypRef Expression
1 nfim.1 . 2  |-  F/ x ph
2 nfim.2 . . 3  |-  F/ x ps
32a1i 11 . 2  |-  ( ph  ->  F/ x ps )
41, 3nfim1 1831 1  |-  F/ x
( ph  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4   F/wnf 1554
This theorem is referenced by:  nfanOLD  1849  nfbiOLD  1858  nfor  1859  nfnf  1868  nfia1  1876  19.38OLD  1896  cbval2  1990  nfmo1  2294  mo  2305  moexex  2352  2mo  2361  2eu4  2366  2eu6  2368  cbvralf  2928  vtocl2gf  3015  vtocl3gf  3016  vtoclgaf  3018  vtocl2gaf  3020  vtocl3gaf  3022  rspct  3047  rspc  3048  ralab2  3101  mob  3118  csbhypf  3288  cbvralcsf  3313  dfss2f  3341  elintab  4063  axrep2  4324  axrep3  4325  nfpo  4510  nffr  4558  reusv2lem4  4729  reusv3  4733  tfis  4836  tfinds  4841  tfindes  4844  findes  4877  fv3  5746  tz6.12c  5752  fvmptss  5815  fvmptdf  5818  fvmptt  5822  fvmptf  5823  fmptco  5903  dff13f  6008  ovmpt2s  6199  ov2gf  6200  ovmpt2df  6207  ov3  6212  dfoprab4f  6407  tfr3  6662  dom2lem  7149  findcard2  7350  ac6sfi  7353  dfac8clem  7915  aceq1  8000  dfac5lem5  8010  zfcndrep  8491  zfcndinf  8495  pwfseqlem4a  8538  pwfseqlem4  8539  uzindOLD  10366  uzind4s  10538  seqof2  11383  rlim2  12292  ello1mpt  12317  o1compt  12383  summolem2a  12511  sumss  12520  o1fsum  12594  prmind2  13092  mreiincl  13823  gsumcom2  15551  bwth  17475  ptcldmpt  17648  cnmptcom  17712  elmptrab  17861  isfildlem  17891  dvmptfsum  19861  dvfsumlem2  19913  dvfsumlem4  19915  dvfsumrlim  19917  dvfsum2  19920  coeeq2  20163  dgrle  20164  rlimcnp  20806  lgseisenlem2  21136  dchrisumlema  21184  dchrisumlem2  21186  dchrisumlem3  21187  isch3  22746  atom1d  23858  mo5f  23974  ssiun2sf  24012  fmptcof2  24078  measiun  24574  lgamgulmlem2  24816  prodmolem2a  25262  fprodn0  25305  setinds  25407  tfisg  25481  wfisg  25486  frinsg  25522  mptelee  25836  subtr  26319  subtr2  26320  fdc1  26452  fphpd  26879  monotuz  27006  monotoddzz  27008  oddcomabszz  27009  setindtrs  27098  aomclem6  27136  flcidc  27358  fmul01  27688  fmuldfeqlem1  27690  fmuldfeq  27691  fmul01lt1lem1  27692  fmul01lt1lem2  27693  climmulf  27708  climexp  27709  climsuse  27712  climrecf  27713  climinff  27715  stoweidlem3  27730  stoweidlem26  27753  stoweidlem31  27758  stoweidlem34  27761  stoweidlem42  27769  stoweidlem43  27770  stoweidlem48  27775  stoweidlem51  27778  stoweidlem59  27786  2reu4a  27945  eu2ndop1stv  27958  bnj1385  29266  bnj1468  29279  bnj110  29291  bnj849  29358  bnj900  29362  bnj981  29383  bnj1014  29393  bnj1123  29417  bnj1128  29421  bnj1384  29463  bnj1489  29487  bnj1497  29491  cdleme31sn1  31240  cdleme32fva  31296  cdlemk36  31772
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-11 1762
This theorem depends on definitions:  df-bi 179  df-ex 1552  df-nf 1555
  Copyright terms: Public domain W3C validator