Theorem nfim 1859

Description: If 𝑥 is not free in 𝜑 and 𝜓, then it is not free in (𝜑 → 𝜓). Inference associated with nfimt 1858. (Contributed by Mario Carneiro, 11-Aug-2016.) (Proof shortened by Wolf Lammen, 2-Jan-2018.) df-nf 1747 changed. (Revised by Wolf Lammen, 17-Sep-2021.)

Hypotheses

Ref	Expression
nfim.1	⊢ Ⅎ𝑥𝜑
nfim.2	⊢ Ⅎ𝑥𝜓

Assertion

Ref	Expression
nfim	⊢ Ⅎ𝑥(𝜑 → 𝜓)

Proof of Theorem nfim

Step	Hyp	Ref	Expression
1		nfim.1	. 2 ⊢ Ⅎ𝑥𝜑
2		nfim.2	. 2 ⊢ Ⅎ𝑥𝜓
3		nfimt 1858	. 2 ⊢ ((Ⅎ𝑥𝜑 ∧ Ⅎ𝑥𝜓) → Ⅎ𝑥(𝜑 → 𝜓))
4	1, 2, 3	mp2an 679	1 ⊢ Ⅎ𝑥(𝜑 → 𝜓)

Syntax hints:   → wi 4  Ⅎwnf 1746

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772

This theorem depends on definitions:  df-bi 199  df-an 388  df-ex 1743  df-nf 1747

This theorem is referenced by:  nfor  1867  nfia1  2088  nfnf1  2089  nfnf  2264  nfsbv  2268  nfsbvOLD  2269  2sb8evOLD  2287  cbval2OLD  2344  mof  2571  mofOLD  2572  nfmo1OLD  2617  moexexvw  2658  2moswapv  2659  moexex  2666  cbvralf  3374  vtocl2gf  3485  vtocl3gf  3486  vtoclgaf  3489  vtocl2gaf  3492  vtocl3gaf  3493  rspct  3524  rspc  3526  ralab2  3601  mob  3621  reu2eqd  3638  reu8nf  3762  csbhypf  3806  cbvralcsf  3819  dfss2f  3848  rspn0  4198  2reu4lem  4346  reusngf  4484  rexreusng  4489  reuprg0  4510  elintab  4758  axrep2  5050  axrep3  5051  reusv2lem4  5153  reusv3  5157  iunopeqop  5264  nfpo  5328  nffr  5378  reuop  5980  wfisg  6019  fv3  6515  fvmptss  6604  fvmptd3f  6607  fvmptt  6612  fvmptf  6613  fmptco  6712  dff13f  6837  ovmpos  7112  ov2gf  7113  ovmpodf  7120  ov3  7125  tfis  7383  tfinds  7388  tfindes  7391  findes  7425  dfoprab4f  7559  offval22  7588  tfr3  7836  dom2lem  8342  findcard2  8549  ac6sfi  8553  dfac8clem  9248  aceq1  9333  dfac5lem5  9343  zfcndrep  9830  zfcndinf  9834  pwfseqlem4a  9877  pwfseqlem4  9878  uzind4s  12119  rabssnn0fi  13166  seqof2  13240  rlim2  14708  ello1mpt  14733  o1compt  14799  summolem2a  14926  sumss  14935  fsumsplitf  14952  o1fsum  15022  prodmolem2a  15142  fprodn0  15187  fproddivf  15195  fprodsplitf  15196  fprodsplit1f  15198  prmind2  15879  mreiincl  16719  gsumcom2  18842  gsummptnn0fz  18850  gsummoncoe1  20169  mdetralt2  20916  mdetunilem2  20920  ptcldmpt  21920  cnmptcom  21984  elmptrab  22133  isfildlem  22163  dvmptfsum  24269  dvfsumlem2  24321  dvfsumlem4  24323  dvfsumrlim  24325  dvfsum2  24328  coeeq2  24529  dgrle  24530  rlimcnp  25239  lgamgulmlem2  25303  lgseisenlem2  25648  dchrisumlema  25760  dchrisumlem2  25762  dchrisumlem3  25763  mptelee  26378  gropd  26513  grstructd  26514  isch3  28791  atom1d  29905  vtocl2d  30007  mo5f  30029  ssiun2sf  30074  ssrelf  30124  fmptcof2  30158  aciunf1lem  30163  nn0min  30277  fsumiunle  30285  esum2dlem  30986  fiunelros  31069  measiun  31113  bnj1385  31743  bnj1468  31756  bnj110  31768  bnj849  31835  bnj900  31839  bnj981  31860  bnj1014  31870  bnj1123  31894  bnj1128  31898  bnj1384  31940  bnj1489  31964  bnj1497  31968  setinds  32513  tfisg  32546  frpoinsg  32572  frinsg  32578  nosupbnd1  32705  nosupbnd2  32707  subtr  33153  subtr2  33154  bj-cbval2v  33552  bj-axrep2  33589  bj-axrep3  33590  mptsnunlem  34026  finxpreclem2  34077  finxpreclem6  34083  ptrest  34310  poimirlem24  34335  poimirlem25  34336  poimirlem26  34337  poimirlem28  34339  fdc1  34441  ac6s6  34872  fsumshftd  35511  cdleme31sn1  36940  cdleme32fva  36996  cdlemk36  37472  fphpd  38787  monotuz  38912  monotoddzz  38914  oddcomabszz  38915  setindtrs  38996  aomclem6  39033  flcidc  39148  rababg  39273  ss2iundf  39345  binomcxplemnotnn0  40081  uzwo4  40712  fiiuncl  40724  disjf1  40846  disjinfi  40857  dmrelrnrel  40894  supxrgere  41009  supxrgelem  41013  supxrge  41014  supxrleubrnmptf  41137  monoordxr  41169  monoord2xr  41171  fsumclf  41260  fsummulc1f  41261  fsumnncl  41262  fsumsplit1  41263  fsumf1of  41265  fsumiunss  41266  fsumreclf  41267  fsumlessf  41268  fsumsermpt  41270  fmul01  41271  fmuldfeqlem1  41273  fmuldfeq  41274  fmul01lt1lem1  41275  fmul01lt1lem2  41276  fprodexp  41285  fprodabs2  41286  fprodcnlem  41290  climmulf  41295  climexp  41296  climsuse  41299  climrecf  41300  climinff  41302  climaddf  41306  mullimc  41307  idlimc  41317  neglimc  41338  addlimc  41339  0ellimcdiv  41340  limclner  41342  climsubmpt  41351  climreclf  41355  climeldmeqmpt  41359  climfveqmpt  41362  fnlimfvre  41365  climfveqf  41371  climfveqmpt3  41373  climeldmeqf  41374  limsupref  41376  limsupbnd1f  41377  climeqf  41379  climeldmeqmpt3  41380  climinf2  41398  climinf2mpt  41405  climinfmpt  41406  limsupmnf  41412  limsupequz  41414  limsupre2  41416  limsupequzmptf  41422  limsupre3  41424  cncfshift  41566  fprodcncf  41593  dvmptmulf  41631  dvnmptdivc  41632  dvnmul  41637  dvmptfprodlem  41638  dvmptfprod  41639  iblspltprt  41667  stoweidlem3  41698  stoweidlem26  41721  stoweidlem31  41726  stoweidlem34  41729  stoweidlem42  41737  stoweidlem43  41738  stoweidlem48  41743  stoweidlem51  41746  stoweidlem59  41754  fourierdlem86  41887  fourierdlem89  41890  fourierdlem91  41892  fourierdlem112  41913  sge0f1o  42074  sge0lempt  42102  sge0iunmptlemfi  42105  sge0iunmptlemre  42107  sge0fodjrnlem  42108  sge0iunmpt  42110  sge0ltfirpmpt2  42118  sge0isummpt2  42124  sge0xaddlem2  42126  sge0xadd  42127  meadjiun  42158  voliunsge0lem  42164  meaiunincf  42175  meaiuninc3  42177  meaiininc  42179  hoimbl2  42357  vonhoire  42364  vonn0ioo2  42382  vonn0icc2  42384  salpreimagelt  42396  salpreimalegt  42398  salpreimagtge  42412  salpreimaltle  42413  salpreimagtlt  42417  2reu8i  42697  eu2ndop1stv  42709  f1oresf1o2  42875  ichreuopeq  42977  reupr  43026  reuopreuprim  43030  2zrngmmgm  43555  nfsetrecs  44130  setrec2fun  44136