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

Theorem nfim 1980
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 1979 1  |-  F/ x
( ph  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4   F/wnf 1661
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-10 1891  ax-12 1909
This theorem depends on definitions:  df-bi 188  df-ex 1658  df-nf 1662
This theorem is referenced by:  nfor  1995  nfnf  2009  nfia1  2014  cbval2  2086  mo2  2279  nfmo1  2281  moexex  2341  cbvralf  2984  vtocl2gf  3077  vtocl3gf  3078  vtoclgaf  3080  vtocl2gaf  3082  vtocl3gaf  3084  rspct  3111  rspc  3112  ralab2  3171  mob  3188  reu2eqd  3203  csbhypf  3350  cbvralcsf  3363  dfss2f  3391  rspn0  3710  elintab  4202  axrep2  4474  axrep3  4475  reusv2lem4  4564  reusv3  4568  nfpo  4715  nffr  4763  wfisg  5370  fv3  5831  tz6.12c  5837  fvmptss  5911  fvmptdf  5914  fvmptt  5918  fvmptf  5919  fmptco  6008  dff13f  6112  ovmpt2s  6371  ov2gf  6372  ovmpt2df  6379  ov3  6384  tfis  6632  tfinds  6637  tfindes  6640  findes  6674  dfoprab4f  6802  offval22  6823  tfr3  7065  dom2lem  7556  findcard2  7757  ac6sfi  7761  dfac8clem  8407  aceq1  8492  dfac5lem5  8502  zfcndrep  8983  zfcndinf  8987  pwfseqlem4a  9030  pwfseqlem4  9031  uzind4s  11163  rabssnn0fi  12141  seqof2  12214  rlim2  13496  ello1mpt  13521  o1compt  13587  summolem2a  13717  sumss  13726  o1fsum  13809  prodmolem2a  13924  fprodn0  13969  fproddivf  13977  fprodsplitf  13978  fprodsplit1f  13980  prmind2  14571  mreiincl  15438  gsumcom2  17543  gsummptnn0fz  17551  gsummoncoe1  18834  mdetralt2  19569  mdetunilem2  19573  ptcldmpt  20564  cnmptcom  20628  elmptrab  20777  isfildlem  20807  dvmptfsum  22862  dvfsumlem2  22914  dvfsumlem4  22916  dvfsumrlim  22918  dvfsum2  22921  coeeq2  23131  dgrle  23132  rlimcnp  23826  lgamgulmlem2  23890  lgseisenlem2  24213  dchrisumlema  24261  dchrisumlem2  24263  dchrisumlem3  24264  mptelee  24860  isch3  26829  atom1d  27941  vtocl2d  28044  mo5f  28055  ssiun2sf  28113  ssrelf  28160  fmptcof2  28198  aciunf1lem  28203  nn0min  28328  esum2dlem  28858  fiunelros  28941  measiun  28985  bnj1385  29589  bnj1468  29602  bnj110  29614  bnj849  29681  bnj900  29685  bnj981  29706  bnj1014  29716  bnj1123  29740  bnj1128  29744  bnj1384  29786  bnj1489  29810  bnj1497  29814  setinds  30368  tfisg  30401  frinsg  30427  subtr  30912  subtr2  30913  bj-cbval2v  31239  bj-axrep2  31311  bj-axrep3  31312  bj-mo3OLD  31354  mptsnunlem  31641  finxpreclem2  31683  finxpreclem6  31689  ptrest  31840  poimirlem24  31865  poimirlem25  31866  poimirlem26  31867  poimirlem28  31869  fdc1  31976  ac6s6  32316  fsumshftd  32429  fsumshftdOLD  32430  cdleme31sn1  33854  cdleme32fva  33910  cdlemk36  34386  fphpd  35565  monotuz  35696  monotoddzz  35698  oddcomabszz  35699  setindtrs  35787  aomclem6  35824  flcidc  35947  rababg  36086  ss2iundf  36158  binomcxplemnotnn0  36612  uzwo4  37302  fiiuncl  37316  disjf1  37355  disjinfi  37366  supxrgere  37447  supxrgelem  37451  supxrge  37452  fsumclf  37523  fsumsplitf  37524  fsummulc1f  37525  fsumnncl  37528  fsumsplit1  37529  fsumf1of  37531  fsumiunss  37532  fsumreclf  37533  fsumlessf  37534  fmul01  37535  fmuldfeqlem1  37537  fmuldfeq  37538  fmul01lt1lem1  37539  fmul01lt1lem2  37540  fprodexp  37551  fprodabs2  37552  climmulf  37559  climexp  37560  climsuse  37564  climrecf  37565  climinff  37567  climinffOLD  37568  climaddf  37572  mullimc  37573  idlimc  37583  neglimc  37605  addlimc  37606  0ellimcdiv  37607  limclner  37609  cncfshift  37628  cncfiooicclem1  37648  fprodcncf  37656  dvmptmulf  37689  dvnmptdivc  37690  dvnmul  37695  dvmptfprodlem  37696  dvmptfprod  37697  iblspltprt  37727  stoweidlem3  37740  stoweidlem26  37763  stoweidlem31  37769  stoweidlem34  37772  stoweidlem42  37780  stoweidlem43  37781  stoweidlem48  37786  stoweidlem51  37789  stoweidlem59  37797  fourierdlem86  37933  fourierdlem89  37936  fourierdlem91  37938  fourierdlem112  37959  sge0f1o  38069  sge0lempt  38097  sge0iunmptlemfi  38100  sge0iunmptlemre  38102  sge0fodjrnlem  38103  sge0iunmpt  38105  sge0ltfirpmpt2  38113  sge0isummpt2  38119  sge0xaddlem2  38121  sge0xadd  38122  meadjiun  38149  2reu4a  38418  eu2ndop1stv  38431  iunopeqop  38807  gropd  38901  grstructd  38902  2zrngmmgm  39531
  Copyright terms: Public domain W3C validator