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

Theorem nfim 1888
Description: If 𝑥 is not free in 𝜑 and 𝜓, then it is not free in (𝜑𝜓). Inference associated with nfimt 1887. (Contributed by Mario Carneiro, 11-Aug-2016.) (Proof shortened by Wolf Lammen, 2-Jan-2018.) df-nf 1776 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 1887 . 2 ((Ⅎ𝑥𝜑 ∧ Ⅎ𝑥𝜓) → Ⅎ𝑥(𝜑𝜓))
41, 2, 3mp2an 688 1 𝑥(𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wnf 1775
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801
This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1772  df-nf 1776
This theorem is referenced by:  nfor  1896  nfia1  2148  nfnf1  2149  nfnf  2337  nfsbv  2341  nfsbvOLD  2342  cbval2vOLD  2356  2sb8evOLD  2368  cbval2OLD  2427  mof  2643  moexexlem  2707  nfabdw  3000  cbvralfw  3438  cbvralf  3440  vtocl2gf  3570  vtocl3gf  3571  vtoclgaf  3573  vtocl2gaf  3576  vtocl3gaf  3577  rspct  3608  rspc  3610  ralab2  3687  ralab2OLD  3688  mob  3707  reu2eqd  3726  reu8nf  3859  csbhypf  3910  cbvralcsf  3924  vtocl2dOLD  3930  dfss2f  3957  rspn0  4312  2reu4lem  4463  reusngf  4606  rexreusng  4611  reuprg0  4632  elintab  4880  axrep2  5185  axrep3  5186  reusv2lem4  5293  reusv3  5297  iunopeqop  5403  nfpo  5473  nffr  5523  reuop  6138  wfisg  6177  fv3  6682  fvmptss  6773  fvmptd3f  6776  fvmptt  6781  fvmptf  6782  fmptco  6884  dff13f  7005  ovmpos  7287  ov2gf  7288  ovmpodf  7295  ov3  7300  tfis  7557  tfinds  7562  tfindes  7565  findes  7600  dfoprab4f  7745  offval22  7774  tfr3  8026  dom2lem  8538  findcard2  8747  ac6sfi  8751  dfac8clem  9447  aceq1  9532  dfac5lem5  9542  zfcndrep  10025  zfcndinf  10029  pwfseqlem4a  10072  pwfseqlem4  10073  uzind4s  12297  rabssnn0fi  13344  seqof2  13418  rlim2  14843  ello1mpt  14868  o1compt  14934  summolem2a  15062  sumss  15071  fsumsplitf  15088  o1fsum  15158  prodmolem2a  15278  fprodn0  15323  fproddivf  15331  fprodsplitf  15332  fprodsplit1f  15334  prmind2  16019  mreiincl  16857  gsumcom2  19026  gsummptnn0fz  19037  gsummoncoe1  20402  mdetralt2  21148  mdetunilem2  21152  ptcldmpt  22152  cnmptcom  22216  elmptrab  22365  isfildlem  22395  dvmptfsum  24501  dvfsumlem2  24553  dvfsumlem4  24555  dvfsumrlim  24557  dvfsum2  24560  coeeq2  24761  dgrle  24762  rlimcnp  25471  lgamgulmlem2  25535  lgseisenlem2  25880  dchrisumlema  25992  dchrisumlem2  25994  dchrisumlem3  25995  mptelee  26609  gropd  26744  grstructd  26745  isch3  28946  atom1d  30058  mo5f  30181  ssiun2sf  30240  ssrelf  30295  fmptcof2  30331  aciunf1lem  30336  nn0min  30464  fsumiunle  30473  esum2dlem  31251  fiunelros  31333  measiun  31377  bnj1385  32004  bnj1468  32018  bnj110  32030  bnj849  32097  bnj900  32101  bnj981  32122  bnj1014  32132  bnj1123  32156  bnj1128  32160  bnj1384  32202  bnj1489  32226  bnj1497  32230  setinds  32921  tfisg  32953  frpoinsg  32979  frinsg  32985  nosupbnd1  33112  nosupbnd2  33114  subtr  33560  subtr2  33561  currysetlem  34154  currysetlem1  34156  mptsnunlem  34502  finxpreclem2  34554  finxpreclem6  34560  ptrest  34773  poimirlem24  34798  poimirlem25  34799  poimirlem26  34800  poimirlem28  34802  fdc1  34904  ac6s6  35333  fsumshftd  35970  cdleme31sn1  37399  cdleme32fva  37455  cdlemk36  37931  fphpd  39293  monotuz  39418  monotoddzz  39420  oddcomabszz  39421  setindtrs  39502  aomclem6  39539  flcidc  39654  rababg  39813  ss2iundf  39884  binomcxplemnotnn0  40568  uzwo4  41195  fiiuncl  41207  disjf1  41323  disjinfi  41334  dmrelrnrel  41370  supxrgere  41481  supxrgelem  41485  supxrge  41486  supxrleubrnmptf  41607  monoordxr  41639  monoord2xr  41641  fsumclf  41730  fsummulc1f  41731  fsumnncl  41732  fsumsplit1  41733  fsumf1of  41735  fsumiunss  41736  fsumreclf  41737  fsumlessf  41738  fsumsermpt  41740  fmul01  41741  fmuldfeqlem1  41743  fmuldfeq  41744  fmul01lt1lem1  41745  fmul01lt1lem2  41746  fprodexp  41755  fprodabs2  41756  fprodcnlem  41760  climmulf  41765  climexp  41766  climsuse  41769  climrecf  41770  climinff  41772  climaddf  41776  mullimc  41777  idlimc  41787  neglimc  41808  addlimc  41809  0ellimcdiv  41810  limclner  41812  climsubmpt  41821  climreclf  41825  climeldmeqmpt  41829  climfveqmpt  41832  fnlimfvre  41835  climfveqf  41841  climfveqmpt3  41843  climeldmeqf  41844  limsupref  41846  limsupbnd1f  41847  climeqf  41849  climeldmeqmpt3  41850  climinf2  41868  climinf2mpt  41875  climinfmpt  41876  limsupmnf  41882  limsupequz  41884  limsupre2  41886  limsupequzmptf  41892  limsupre3  41894  cncfshift  42037  fprodcncf  42064  dvmptmulf  42102  dvnmptdivc  42103  dvnmul  42108  dvmptfprodlem  42109  dvmptfprod  42110  iblspltprt  42138  stoweidlem3  42169  stoweidlem26  42192  stoweidlem31  42197  stoweidlem34  42200  stoweidlem42  42208  stoweidlem43  42209  stoweidlem48  42214  stoweidlem51  42217  stoweidlem59  42225  fourierdlem86  42358  fourierdlem89  42361  fourierdlem91  42363  fourierdlem112  42384  sge0f1o  42545  sge0lempt  42573  sge0iunmptlemfi  42576  sge0iunmptlemre  42578  sge0fodjrnlem  42579  sge0iunmpt  42581  sge0ltfirpmpt2  42589  sge0isummpt2  42595  sge0xaddlem2  42597  sge0xadd  42598  meadjiun  42629  voliunsge0lem  42635  meaiunincf  42646  meaiuninc3  42648  meaiininc  42650  hoimbl2  42828  vonhoire  42835  vonn0ioo2  42853  vonn0icc2  42855  salpreimagelt  42867  salpreimalegt  42869  salpreimagtge  42883  salpreimaltle  42884  salpreimagtlt  42888  2reu8i  43193  eu2ndop1stv  43205  f1oresf1o2  43371  ichreuopeq  43482  reupr  43531  reuopreuprim  43535  2zrngmmgm  44115  nfsetrecs  44687  setrec2fun  44693
  Copyright terms: Public domain W3C validator