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

Theorem nfim 1904
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 1903 1  |-  F/ x
( ph  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4   F/wnf 1601
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616  ax-5 1689  ax-6 1732  ax-7 1774  ax-10 1821  ax-12 1838
This theorem depends on definitions:  df-bi 185  df-ex 1598  df-nf 1602
This theorem is referenced by:  nfor  1919  nfnf  1933  nfia1  1938  cbval2  2011  mo2  2277  nfmo1  2279  mo3OLD  2308  moexex  2347  2eu4OLD  2365  2eu6OLD  2368  cbvralf  3062  vtocl2gf  3153  vtocl3gf  3154  vtoclgaf  3156  vtocl2gaf  3158  vtocl3gaf  3160  rspct  3187  rspc  3188  ralab2  3248  mob  3265  reu2eqd  3280  csbhypf  3436  cbvralcsf  3449  dfss2f  3477  rspn0  3779  elintab  4278  axrep2  4546  axrep3  4547  reusv2lem4  4637  reusv3  4641  nfpo  4791  nffr  4839  fv3  5865  tz6.12c  5871  fvmptss  5945  fvmptdf  5948  fvmptt  5952  fvmptf  5953  fmptco  6045  dff13f  6148  ovmpt2s  6407  ov2gf  6408  ovmpt2df  6415  ov3  6420  tfis  6670  tfinds  6675  tfindes  6678  findes  6711  dfoprab4f  6839  offval22  6860  tfr3  7066  dom2lem  7553  findcard2  7758  ac6sfi  7762  dfac8clem  8411  aceq1  8496  dfac5lem5  8506  zfcndrep  8990  zfcndinf  8994  pwfseqlem4a  9037  pwfseqlem4  9038  uzindOLD  10958  uzind4s  11145  rabssnn0fi  12069  seqof2  12139  rlim2  13293  ello1mpt  13318  o1compt  13384  summolem2a  13511  sumss  13520  o1fsum  13601  prmind2  14100  mreiincl  14865  gsumcom2  16872  gsummptnn0fz  16883  gsummoncoe1  18214  mdetralt2  18978  mdetunilem2  18982  bwthOLD  19777  ptcldmpt  19981  cnmptcom  20045  elmptrab  20194  isfildlem  20224  dvmptfsum  22242  dvfsumlem2  22294  dvfsumlem4  22296  dvfsumrlim  22298  dvfsum2  22301  coeeq2  22505  dgrle  22506  rlimcnp  23160  lgseisenlem2  23490  dchrisumlema  23538  dchrisumlem2  23540  dchrisumlem3  23541  mptelee  24063  isch3  26024  atom1d  27137  mo5f  27248  ssiun2sf  27292  ssrelf  27331  fmptcof2  27367  nn0min  27477  measiun  28055  lgamgulmlem2  28438  prodmolem2a  29034  fprodn0  29077  setinds  29178  tfisg  29252  wfisg  29257  frinsg  29293  ptrest  30016  subtr  30100  subtr2  30101  fdc1  30207  ac6s6  30548  fphpd  30718  monotuz  30845  monotoddzz  30847  oddcomabszz  30848  setindtrs  30935  aomclem6  30973  flcidc  31092  fmul01  31498  fmuldfeqlem1  31500  fmuldfeq  31501  fmul01lt1lem1  31502  fmul01lt1lem2  31503  climmulf  31514  climexp  31515  climsuse  31518  climrecf  31519  climinff  31521  climaddf  31525  mullimc  31526  idlimc  31536  neglimc  31557  addlimc  31558  0ellimcdiv  31559  limclner  31561  cncfshift  31579  cncfiooicclem1  31599  iblspltprt  31658  stoweidlem3  31670  stoweidlem26  31693  stoweidlem31  31698  stoweidlem34  31701  stoweidlem42  31709  stoweidlem43  31710  stoweidlem48  31715  stoweidlem51  31718  stoweidlem59  31726  fourierdlem86  31860  fourierdlem89  31863  fourierdlem91  31865  fourierdlem112  31886  2reu4a  32028  eu2ndop1stv  32041  2zrngmmgm  32452  bnj1385  33598  bnj1468  33611  bnj110  33623  bnj849  33690  bnj900  33694  bnj981  33715  bnj1014  33725  bnj1123  33749  bnj1128  33753  bnj1384  33795  bnj1489  33819  bnj1497  33823  bj-cbval2v  34016  bj-axrep2  34087  bj-axrep3  34088  fsumshftd  34384  fsumshftdOLD  34385  cdleme31sn1  35809  cdleme32fva  35865  cdlemk36  36341
  Copyright terms: Public domain W3C validator