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

Theorem nfim 1823
Description: If 𝑥 is not free in 𝜑 and 𝜓, it is not free in (𝜑𝜓). Inference associated with nfimt 1819. (Contributed by Mario Carneiro, 11-Aug-2016.) (Proof shortened by Wolf Lammen, 2-Jan-2018.) df-nf 1708 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 1820 . 2 ((Ⅎ𝑥𝜑 ∧ Ⅎ𝑥𝜓) → Ⅎ𝑥(𝜑𝜓))
41, 2, 3mp2an 707 1 𝑥(𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wnf 1706
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735
This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1703  df-nf 1708
This theorem is referenced by:  nfanOLD  1827  nfor  1832  nfia1  2028  nfnf1  2029  nfnf  2156  cbval2  2277  mo2  2477  nfmo1  2479  moexex  2539  cbvralf  3160  vtocl2gf  3263  vtocl3gf  3264  vtoclgaf  3266  vtocl2gaf  3268  vtocl3gaf  3270  rspct  3297  rspc  3298  ralab2  3365  mob  3382  reu2eqd  3397  csbhypf  3545  cbvralcsf  3558  dfss2f  3586  rspn0  3926  elintab  4478  axrep2  4764  axrep3  4765  reusv2lem4  4863  reusv3  4867  iunopeqop  4971  nfpo  5030  nffr  5078  wfisg  5703  fv3  6193  tz6.12c  6200  fvmptss  6279  fvmptdf  6282  fvmptt  6286  fvmptf  6287  fmptco  6382  dff13f  6498  ovmpt2s  6769  ov2gf  6770  ovmpt2df  6777  ov3  6782  tfis  7039  tfinds  7044  tfindes  7047  findes  7081  dfoprab4f  7211  offval22  7238  tfr3  7480  dom2lem  7980  findcard2  8185  ac6sfi  8189  dfac8clem  8840  aceq1  8925  dfac5lem5  8935  zfcndrep  9421  zfcndinf  9425  pwfseqlem4a  9468  pwfseqlem4  9469  uzind4s  11733  rabssnn0fi  12768  seqof2  12842  rlim2  14208  ello1mpt  14233  o1compt  14299  summolem2a  14427  sumss  14436  fsumsplitf  14453  o1fsum  14526  prodmolem2a  14645  fprodn0  14690  fproddivf  14699  fprodsplitf  14700  fprodsplit1f  14702  prmind2  15379  mreiincl  16237  gsumcom2  18355  gsummptnn0fz  18363  gsummoncoe1  19655  mdetralt2  20396  mdetunilem2  20400  ptcldmpt  21398  cnmptcom  21462  elmptrab  21611  isfildlem  21642  dvmptfsum  23719  dvfsumlem2  23771  dvfsumlem4  23773  dvfsumrlim  23775  dvfsum2  23778  coeeq2  23979  dgrle  23980  rlimcnp  24673  lgamgulmlem2  24737  lgseisenlem2  25082  dchrisumlema  25158  dchrisumlem2  25160  dchrisumlem3  25161  mptelee  25756  gropd  25904  grstructd  25905  isch3  28068  atom1d  29182  vtocl2d  29285  mo5f  29296  ssiun2sf  29350  ssrelf  29397  fmptcof2  29430  aciunf1lem  29435  nn0min  29541  fsumiunle  29549  esum2dlem  30128  fiunelros  30211  measiun  30255  bnj1385  30877  bnj1468  30890  bnj110  30902  bnj849  30969  bnj900  30973  bnj981  30994  bnj1014  31004  bnj1123  31028  bnj1128  31032  bnj1384  31074  bnj1489  31098  bnj1497  31102  setinds  31657  tfisg  31690  frinsg  31716  nosupbnd1  31834  nosupbnd2  31836  subtr  32283  subtr2  32284  bj-cbval2v  32712  bj-axrep2  32764  bj-axrep3  32765  bj-mo3OLD  32807  mptsnunlem  33156  finxpreclem2  33198  finxpreclem6  33204  ptrest  33379  poimirlem24  33404  poimirlem25  33405  poimirlem26  33406  poimirlem28  33408  fdc1  33513  ac6s6  33951  fsumshftd  34056  fsumshftdOLD  34057  cdleme31sn1  35488  cdleme32fva  35544  cdlemk36  36020  fphpd  37199  monotuz  37325  monotoddzz  37327  oddcomabszz  37328  setindtrs  37411  aomclem6  37448  flcidc  37563  rababg  37698  ss2iundf  37770  binomcxplemnotnn0  38375  uzwo4  39041  fiiuncl  39054  disjf1  39185  disjinfi  39196  dmrelrnrel  39235  supxrgere  39362  supxrgelem  39366  supxrge  39367  supxrleubrnmptf  39493  fsumclf  39601  fsummulc1f  39602  fsumnncl  39603  fsumsplit1  39604  fsumf1of  39606  fsumiunss  39607  fsumreclf  39608  fsumlessf  39609  fsumsermpt  39611  fmul01  39612  fmuldfeqlem1  39614  fmuldfeq  39615  fmul01lt1lem1  39616  fmul01lt1lem2  39617  fprodexp  39626  fprodabs2  39627  fprodcnlem  39631  climmulf  39636  climexp  39637  climsuse  39640  climrecf  39641  climinff  39643  climaddf  39647  mullimc  39648  idlimc  39658  neglimc  39679  addlimc  39680  0ellimcdiv  39681  limclner  39683  climsubmpt  39692  climreclf  39696  climeldmeqmpt  39700  climfveqmpt  39703  fnlimfvre  39706  climfveqf  39712  climfveqmpt3  39714  climeldmeqf  39715  limsupref  39717  limsupbnd1f  39718  climeqf  39720  climeldmeqmpt3  39721  climinf2  39739  climinf2mpt  39746  climinfmpt  39747  limsupmnf  39753  limsupequz  39755  limsupre2  39757  limsupequzmptf  39763  limsupre3  39765  cncfshift  39850  cncfiooicclem1  39869  fprodcncf  39877  dvmptmulf  39915  dvnmptdivc  39916  dvnmul  39921  dvmptfprodlem  39922  dvmptfprod  39923  iblspltprt  39952  stoweidlem3  39983  stoweidlem26  40006  stoweidlem31  40011  stoweidlem34  40014  stoweidlem42  40022  stoweidlem43  40023  stoweidlem48  40028  stoweidlem51  40031  stoweidlem59  40039  fourierdlem86  40172  fourierdlem89  40175  fourierdlem91  40177  fourierdlem112  40198  sge0f1o  40362  sge0lempt  40390  sge0iunmptlemfi  40393  sge0iunmptlemre  40395  sge0fodjrnlem  40396  sge0iunmpt  40398  sge0ltfirpmpt2  40406  sge0isummpt2  40412  sge0xaddlem2  40414  sge0xadd  40415  meadjiun  40446  voliunsge0lem  40452  meaiininc  40464  hoimbl2  40642  vonhoire  40649  vonn0ioo2  40667  vonn0icc2  40669  salpreimagelt  40681  salpreimalegt  40683  salpreimagtge  40697  salpreimaltle  40698  salpreimagtlt  40702  2reu4a  40952  eu2ndop1stv  40965  2zrngmmgm  41711  nfsetrecs  42198  setrec2fun  42204
  Copyright terms: Public domain W3C validator