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

Theorem nfim 1865
Description: If 𝑥 is not free in 𝜑 and 𝜓, it is not free in (𝜑𝜓). Inference associated with nfimt 1861. (Contributed by Mario Carneiro, 11-Aug-2016.) (Proof shortened by Wolf Lammen, 2-Jan-2018.) df-nf 1750 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 nfimt2 1862 . 2 ((Ⅎ𝑥𝜑 ∧ Ⅎ𝑥𝜓) → Ⅎ𝑥(𝜑𝜓))
41, 2, 3mp2an 708 1 𝑥(𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wnf 1748
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777
This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1745  df-nf 1750
This theorem is referenced by:  nfanOLD  1869  nfor  1874  nfia1  2070  nfnf1  2071  nfnf  2196  cbval2  2315  mo2  2507  nfmo1  2509  moexex  2570  cbvralf  3195  vtocl2gf  3299  vtocl3gf  3300  vtoclgaf  3302  vtocl2gaf  3304  vtocl3gaf  3306  rspct  3333  rspc  3334  ralab2  3404  mob  3421  reu2eqd  3436  reu8nf  3549  csbhypf  3585  cbvralcsf  3598  dfss2f  3627  rspn0  3967  elintab  4519  axrep2  4806  axrep3  4807  reusv2lem4  4902  reusv3  4906  iunopeqop  5010  nfpo  5069  nffr  5117  wfisg  5753  fv3  6244  tz6.12c  6251  fvmptss  6331  fvmptd3f  6334  fvmptt  6339  fvmptf  6340  fmptco  6436  dff13f  6553  ovmpt2s  6826  ov2gf  6827  ovmpt2df  6834  ov3  6839  tfis  7096  tfinds  7101  tfindes  7104  findes  7138  dfoprab4f  7270  offval22  7298  tfr3  7540  dom2lem  8037  findcard2  8241  ac6sfi  8245  dfac8clem  8893  aceq1  8978  dfac5lem5  8988  zfcndrep  9474  zfcndinf  9478  pwfseqlem4a  9521  pwfseqlem4  9522  uzind4s  11786  rabssnn0fi  12825  seqof2  12899  rlim2  14271  ello1mpt  14296  o1compt  14362  summolem2a  14490  sumss  14499  fsumsplitf  14516  o1fsum  14589  prodmolem2a  14708  fprodn0  14753  fproddivf  14762  fprodsplitf  14763  fprodsplit1f  14765  prmind2  15445  mreiincl  16303  gsumcom2  18420  gsummptnn0fz  18428  gsummoncoe1  19722  mdetralt2  20463  mdetunilem2  20467  ptcldmpt  21465  cnmptcom  21529  elmptrab  21678  isfildlem  21708  dvmptfsum  23783  dvfsumlem2  23835  dvfsumlem4  23837  dvfsumrlim  23839  dvfsum2  23842  coeeq2  24043  dgrle  24044  rlimcnp  24737  lgamgulmlem2  24801  lgseisenlem2  25146  dchrisumlema  25222  dchrisumlem2  25224  dchrisumlem3  25225  mptelee  25820  gropd  25968  grstructd  25969  isch3  28226  atom1d  29340  vtocl2d  29442  mo5f  29452  ssiun2sf  29504  ssrelf  29553  fmptcof2  29585  aciunf1lem  29590  nn0min  29695  fsumiunle  29703  esum2dlem  30282  fiunelros  30365  measiun  30409  bnj1385  31029  bnj1468  31042  bnj110  31054  bnj849  31121  bnj900  31125  bnj981  31146  bnj1014  31156  bnj1123  31180  bnj1128  31184  bnj1384  31226  bnj1489  31250  bnj1497  31254  setinds  31807  tfisg  31840  frpoinsg  31866  frinsg  31870  nosupbnd1  31985  nosupbnd2  31987  subtr  32433  subtr2  32434  bj-cbval2v  32862  bj-axrep2  32914  bj-axrep3  32915  bj-mo3OLD  32957  mptsnunlem  33315  finxpreclem2  33357  finxpreclem6  33363  ptrest  33538  poimirlem24  33563  poimirlem25  33564  poimirlem26  33565  poimirlem28  33567  fdc1  33672  ac6s6  34110  fsumshftd  34556  cdleme31sn1  35986  cdleme32fva  36042  cdlemk36  36518  fphpd  37697  monotuz  37823  monotoddzz  37825  oddcomabszz  37826  setindtrs  37909  aomclem6  37946  flcidc  38061  rababg  38196  ss2iundf  38268  binomcxplemnotnn0  38872  uzwo4  39535  fiiuncl  39548  disjf1  39683  disjinfi  39694  dmrelrnrel  39733  supxrgere  39862  supxrgelem  39866  supxrge  39867  supxrleubrnmptf  39993  monoordxr  40026  monoord2xr  40028  fsumclf  40119  fsummulc1f  40120  fsumnncl  40121  fsumsplit1  40122  fsumf1of  40124  fsumiunss  40125  fsumreclf  40126  fsumlessf  40127  fsumsermpt  40129  fmul01  40130  fmuldfeqlem1  40132  fmuldfeq  40133  fmul01lt1lem1  40134  fmul01lt1lem2  40135  fprodexp  40144  fprodabs2  40145  fprodcnlem  40149  climmulf  40154  climexp  40155  climsuse  40158  climrecf  40159  climinff  40161  climaddf  40165  mullimc  40166  idlimc  40176  neglimc  40197  addlimc  40198  0ellimcdiv  40199  limclner  40201  climsubmpt  40210  climreclf  40214  climeldmeqmpt  40218  climfveqmpt  40221  fnlimfvre  40224  climfveqf  40230  climfveqmpt3  40232  climeldmeqf  40233  limsupref  40235  limsupbnd1f  40236  climeqf  40238  climeldmeqmpt3  40239  climinf2  40257  climinf2mpt  40264  climinfmpt  40265  limsupmnf  40271  limsupequz  40273  limsupre2  40275  limsupequzmptf  40281  limsupre3  40283  cncfshift  40405  cncfiooicclem1  40424  fprodcncf  40432  dvmptmulf  40470  dvnmptdivc  40471  dvnmul  40476  dvmptfprodlem  40477  dvmptfprod  40478  iblspltprt  40507  stoweidlem3  40538  stoweidlem26  40561  stoweidlem31  40566  stoweidlem34  40569  stoweidlem42  40577  stoweidlem43  40578  stoweidlem48  40583  stoweidlem51  40586  stoweidlem59  40594  fourierdlem86  40727  fourierdlem89  40730  fourierdlem91  40732  fourierdlem112  40753  sge0f1o  40917  sge0lempt  40945  sge0iunmptlemfi  40948  sge0iunmptlemre  40950  sge0fodjrnlem  40951  sge0iunmpt  40953  sge0ltfirpmpt2  40961  sge0isummpt2  40967  sge0xaddlem2  40969  sge0xadd  40970  meadjiun  41001  voliunsge0lem  41007  meaiunincf  41018  meaiuninc3  41020  meaiininc  41022  hoimbl2  41200  vonhoire  41207  vonn0ioo2  41225  vonn0icc2  41227  salpreimagelt  41239  salpreimalegt  41241  salpreimagtge  41255  salpreimaltle  41256  salpreimagtlt  41260  2reu4a  41510  eu2ndop1stv  41523  2zrngmmgm  42271  nfsetrecs  42758  setrec2fun  42764
  Copyright terms: Public domain W3C validator