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

Theorem nfim 1987
Description: If 𝑥 is not free in 𝜑 and 𝜓, it is not free in (𝜑𝜓). Inference associated with nfimt 1984. (Contributed by Mario Carneiro, 11-Aug-2016.) (Proof shortened by Wolf Lammen, 2-Jan-2018.) df-nf 1864 changed. (Revised by Wolf Lammen, 17-Sep-2021.)
Hypotheses
Ref Expression
nfim.1 𝑥𝜑
nfim.2 𝑥𝜓
Assertion
Ref Expression
nfim 𝑥(𝜑𝜓)

Proof of Theorem nfim
StepHypRef Expression
1 nfim.1 . 2 𝑥𝜑
2 nfim.2 . 2 𝑥𝜓
3 nfimt 1984 . 2 ((Ⅎ𝑥𝜑 ∧ Ⅎ𝑥𝜓) → Ⅎ𝑥(𝜑𝜓))
41, 2, 3mp2an 675 1 𝑥(𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wnf 1863
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894
This theorem depends on definitions:  df-bi 198  df-an 385  df-ex 1860  df-nf 1864
This theorem is referenced by:  nfanOLD  1991  nfor  1996  nfia1  2197  nfnf1  2198  nfnf  2334  cbval2  2450  mo2  2639  nfmo1  2641  moexex  2703  cbvralf  3352  vtocl2gf  3459  vtocl3gf  3460  vtoclgaf  3462  vtocl2gaf  3464  vtocl3gaf  3466  rspct  3493  rspc  3494  ralab2  3565  mob  3584  reu2eqd  3599  reu8nf  3709  csbhypf  3745  cbvralcsf  3758  dfss2f  3787  rspn0  4133  elintab  4678  axrep2  4965  axrep3  4966  reusv2lem4  5068  reusv3  5072  iunopeqop  5174  nfpo  5235  nffr  5283  wfisg  5926  fv3  6424  fvmptss  6511  fvmptd3f  6514  fvmptt  6519  fvmptf  6520  fmptco  6617  dff13f  6735  ovmpt2s  7012  ov2gf  7013  ovmpt2df  7020  ov3  7025  tfis  7282  tfinds  7287  tfindes  7290  findes  7324  dfoprab4f  7456  offval22  7485  tfr3  7729  dom2lem  8230  findcard2  8437  ac6sfi  8441  dfac8clem  9136  aceq1  9221  dfac5lem5  9231  zfcndrep  9719  zfcndinf  9723  pwfseqlem4a  9766  pwfseqlem4  9767  uzind4s  11964  rabssnn0fi  13007  seqof2  13080  rlim2  14448  ello1mpt  14473  o1compt  14539  summolem2a  14667  sumss  14676  fsumsplitf  14693  o1fsum  14765  prodmolem2a  14883  fprodn0  14928  fproddivf  14936  fprodsplitf  14937  fprodsplit1f  14939  prmind2  15614  mreiincl  16459  gsumcom2  18573  gsummptnn0fz  18581  gsummptnn0fzOLD  18582  gsummoncoe1  19880  mdetralt2  20624  mdetunilem2  20628  ptcldmpt  21629  cnmptcom  21693  elmptrab  21842  isfildlem  21872  dvmptfsum  23950  dvfsumlem2  24002  dvfsumlem4  24004  dvfsumrlim  24006  dvfsum2  24009  coeeq2  24210  dgrle  24211  rlimcnp  24904  lgamgulmlem2  24968  lgseisenlem2  25313  dchrisumlema  25389  dchrisumlem2  25391  dchrisumlem3  25392  mptelee  25987  gropd  26135  grstructd  26136  isch3  28424  atom1d  29538  vtocl2d  29640  mo5f  29650  ssiun2sf  29701  ssrelf  29750  fmptcof2  29782  aciunf1lem  29787  nn0min  29892  fsumiunle  29900  esum2dlem  30477  fiunelros  30560  measiun  30604  bnj1385  31224  bnj1468  31237  bnj110  31249  bnj849  31316  bnj900  31320  bnj981  31341  bnj1014  31351  bnj1123  31375  bnj1128  31379  bnj1384  31421  bnj1489  31445  bnj1497  31449  setinds  32001  tfisg  32034  frpoinsg  32060  frinsg  32064  nosupbnd1  32179  nosupbnd2  32181  subtr  32627  subtr2  32628  bj-cbval2v  33049  bj-axrep2  33101  bj-axrep3  33102  bj-mo3OLD  33143  mptsnunlem  33500  finxpreclem2  33541  finxpreclem6  33547  ptrest  33719  poimirlem24  33744  poimirlem25  33745  poimirlem26  33746  poimirlem28  33748  fdc1  33851  ac6s6  34288  fsumshftd  34729  cdleme31sn1  36160  cdleme32fva  36216  cdlemk36  36692  fphpd  37880  monotuz  38005  monotoddzz  38007  oddcomabszz  38008  setindtrs  38091  aomclem6  38128  flcidc  38243  rababg  38377  ss2iundf  38449  binomcxplemnotnn0  39053  uzwo4  39712  fiiuncl  39725  disjf1  39856  disjinfi  39867  dmrelrnrel  39904  supxrgere  40027  supxrgelem  40031  supxrge  40032  supxrleubrnmptf  40157  monoordxr  40190  monoord2xr  40192  fsumclf  40279  fsummulc1f  40280  fsumnncl  40281  fsumsplit1  40282  fsumf1of  40284  fsumiunss  40285  fsumreclf  40286  fsumlessf  40287  fsumsermpt  40289  fmul01  40290  fmuldfeqlem1  40292  fmuldfeq  40293  fmul01lt1lem1  40294  fmul01lt1lem2  40295  fprodexp  40304  fprodabs2  40305  fprodcnlem  40309  climmulf  40314  climexp  40315  climsuse  40318  climrecf  40319  climinff  40321  climaddf  40325  mullimc  40326  idlimc  40336  neglimc  40357  addlimc  40358  0ellimcdiv  40359  limclner  40361  climsubmpt  40370  climreclf  40374  climeldmeqmpt  40378  climfveqmpt  40381  fnlimfvre  40384  climfveqf  40390  climfveqmpt3  40392  climeldmeqf  40393  limsupref  40395  limsupbnd1f  40396  climeqf  40398  climeldmeqmpt3  40399  climinf2  40417  climinf2mpt  40424  climinfmpt  40425  limsupmnf  40431  limsupequz  40433  limsupre2  40435  limsupequzmptf  40441  limsupre3  40443  cncfshift  40565  cncfiooicclem1  40584  fprodcncf  40592  dvmptmulf  40630  dvnmptdivc  40631  dvnmul  40636  dvmptfprodlem  40637  dvmptfprod  40638  iblspltprt  40666  stoweidlem3  40697  stoweidlem26  40720  stoweidlem31  40725  stoweidlem34  40728  stoweidlem42  40736  stoweidlem43  40737  stoweidlem48  40742  stoweidlem51  40745  stoweidlem59  40753  fourierdlem86  40886  fourierdlem89  40889  fourierdlem91  40891  fourierdlem112  40912  sge0f1o  41076  sge0lempt  41104  sge0iunmptlemfi  41107  sge0iunmptlemre  41109  sge0fodjrnlem  41110  sge0iunmpt  41112  sge0ltfirpmpt2  41120  sge0isummpt2  41126  sge0xaddlem2  41128  sge0xadd  41129  meadjiun  41160  voliunsge0lem  41166  meaiunincf  41177  meaiuninc3  41179  meaiininc  41181  hoimbl2  41359  vonhoire  41366  vonn0ioo2  41384  vonn0icc2  41386  salpreimagelt  41398  salpreimalegt  41400  salpreimagtge  41414  salpreimaltle  41415  salpreimagtlt  41419  2reu4a  41699  eu2ndop1stv  41712  f1oresf1o2  41879  2zrngmmgm  42512  nfsetrecs  42999  setrec2fun  43005
  Copyright terms: Public domain W3C validator