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

Theorem nfim 1977
Description: If 𝑥 is not free in 𝜑 and 𝜓, it is not free in (𝜑𝜓). Inference associated with nfimt 1974. (Contributed by Mario Carneiro, 11-Aug-2016.) (Proof shortened by Wolf Lammen, 2-Jan-2018.) df-nf 1858 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 1974 . 2 ((Ⅎ𝑥𝜑 ∧ Ⅎ𝑥𝜓) → Ⅎ𝑥(𝜑𝜓))
41, 2, 3mp2an 672 1 𝑥(𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wnf 1856
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885
This theorem depends on definitions:  df-bi 197  df-an 383  df-ex 1853  df-nf 1858
This theorem is referenced by:  nfanOLD  1981  nfor  1986  nfia1  2186  nfnf1  2187  nfnf  2322  cbval2  2438  mo2  2627  nfmo1  2629  moexex  2690  cbvralf  3314  vtocl2gf  3419  vtocl3gf  3420  vtoclgaf  3422  vtocl2gaf  3424  vtocl3gaf  3426  rspct  3453  rspc  3454  ralab2  3523  mob  3540  reu2eqd  3555  reu8nf  3665  csbhypf  3701  cbvralcsf  3714  dfss2f  3743  rspn0  4081  elintab  4622  axrep2  4907  axrep3  4908  reusv2lem4  5001  reusv3  5005  iunopeqop  5114  nfpo  5175  nffr  5223  wfisg  5858  fv3  6347  tz6.12c  6354  fvmptss  6434  fvmptd3f  6437  fvmptt  6442  fvmptf  6443  fmptco  6539  dff13f  6656  ovmpt2s  6931  ov2gf  6932  ovmpt2df  6939  ov3  6944  tfis  7201  tfinds  7206  tfindes  7209  findes  7243  dfoprab4f  7375  offval22  7404  tfr3  7648  dom2lem  8149  findcard2  8356  ac6sfi  8360  dfac8clem  9055  aceq1  9140  dfac5lem5  9150  zfcndrep  9638  zfcndinf  9642  pwfseqlem4a  9685  pwfseqlem4  9686  uzind4s  11950  rabssnn0fi  12993  seqof2  13066  rlim2  14435  ello1mpt  14460  o1compt  14526  summolem2a  14654  sumss  14663  fsumsplitf  14680  o1fsum  14752  prodmolem2a  14871  fprodn0  14916  fproddivf  14924  fprodsplitf  14925  fprodsplit1f  14927  prmind2  15605  mreiincl  16464  gsumcom2  18581  gsummptnn0fz  18589  gsummptnn0fzOLD  18590  gsummoncoe1  19889  mdetralt2  20633  mdetunilem2  20637  ptcldmpt  21638  cnmptcom  21702  elmptrab  21851  isfildlem  21881  dvmptfsum  23958  dvfsumlem2  24010  dvfsumlem4  24012  dvfsumrlim  24014  dvfsum2  24017  coeeq2  24218  dgrle  24219  rlimcnp  24913  lgamgulmlem2  24977  lgseisenlem2  25322  dchrisumlema  25398  dchrisumlem2  25400  dchrisumlem3  25401  mptelee  25996  gropd  26144  grstructd  26145  isch3  28438  atom1d  29552  vtocl2d  29654  mo5f  29664  ssiun2sf  29716  ssrelf  29765  fmptcof2  29797  aciunf1lem  29802  nn0min  29907  fsumiunle  29915  esum2dlem  30494  fiunelros  30577  measiun  30621  bnj1385  31241  bnj1468  31254  bnj110  31266  bnj849  31333  bnj900  31337  bnj981  31358  bnj1014  31368  bnj1123  31392  bnj1128  31396  bnj1384  31438  bnj1489  31462  bnj1497  31466  setinds  32019  tfisg  32052  frpoinsg  32078  frinsg  32082  nosupbnd1  32197  nosupbnd2  32199  subtr  32645  subtr2  32646  bj-cbval2v  33073  bj-axrep2  33125  bj-axrep3  33126  bj-mo3OLD  33167  mptsnunlem  33522  finxpreclem2  33564  finxpreclem6  33570  ptrest  33741  poimirlem24  33766  poimirlem25  33767  poimirlem26  33768  poimirlem28  33770  fdc1  33874  ac6s6  34312  fsumshftd  34760  cdleme31sn1  36190  cdleme32fva  36246  cdlemk36  36722  fphpd  37906  monotuz  38032  monotoddzz  38034  oddcomabszz  38035  setindtrs  38118  aomclem6  38155  flcidc  38270  rababg  38405  ss2iundf  38477  binomcxplemnotnn0  39081  uzwo4  39742  fiiuncl  39755  disjf1  39889  disjinfi  39900  dmrelrnrel  39937  supxrgere  40065  supxrgelem  40069  supxrge  40070  supxrleubrnmptf  40196  monoordxr  40229  monoord2xr  40231  fsumclf  40319  fsummulc1f  40320  fsumnncl  40321  fsumsplit1  40322  fsumf1of  40324  fsumiunss  40325  fsumreclf  40326  fsumlessf  40327  fsumsermpt  40329  fmul01  40330  fmuldfeqlem1  40332  fmuldfeq  40333  fmul01lt1lem1  40334  fmul01lt1lem2  40335  fprodexp  40344  fprodabs2  40345  fprodcnlem  40349  climmulf  40354  climexp  40355  climsuse  40358  climrecf  40359  climinff  40361  climaddf  40365  mullimc  40366  idlimc  40376  neglimc  40397  addlimc  40398  0ellimcdiv  40399  limclner  40401  climsubmpt  40410  climreclf  40414  climeldmeqmpt  40418  climfveqmpt  40421  fnlimfvre  40424  climfveqf  40430  climfveqmpt3  40432  climeldmeqf  40433  limsupref  40435  limsupbnd1f  40436  climeqf  40438  climeldmeqmpt3  40439  climinf2  40457  climinf2mpt  40464  climinfmpt  40465  limsupmnf  40471  limsupequz  40473  limsupre2  40475  limsupequzmptf  40481  limsupre3  40483  cncfshift  40605  cncfiooicclem1  40624  fprodcncf  40632  dvmptmulf  40670  dvnmptdivc  40671  dvnmul  40676  dvmptfprodlem  40677  dvmptfprod  40678  iblspltprt  40706  stoweidlem3  40737  stoweidlem26  40760  stoweidlem31  40765  stoweidlem34  40768  stoweidlem42  40776  stoweidlem43  40777  stoweidlem48  40782  stoweidlem51  40785  stoweidlem59  40793  fourierdlem86  40926  fourierdlem89  40929  fourierdlem91  40931  fourierdlem112  40952  sge0f1o  41116  sge0lempt  41144  sge0iunmptlemfi  41147  sge0iunmptlemre  41149  sge0fodjrnlem  41150  sge0iunmpt  41152  sge0ltfirpmpt2  41160  sge0isummpt2  41166  sge0xaddlem2  41168  sge0xadd  41169  meadjiun  41200  voliunsge0lem  41206  meaiunincf  41217  meaiuninc3  41219  meaiininc  41221  hoimbl2  41399  vonhoire  41406  vonn0ioo2  41424  vonn0icc2  41426  salpreimagelt  41438  salpreimalegt  41440  salpreimagtge  41454  salpreimaltle  41455  salpreimagtlt  41459  2reu4a  41709  eu2ndop1stv  41722  f1oresf1o2  41833  2zrngmmgm  42474  nfsetrecs  42961  setrec2fun  42967
  Copyright terms: Public domain W3C validator