Theorem nfim 1899

Description: If 𝑥 is not free in 𝜑 and 𝜓, then it is not free in (𝜑 → 𝜓). Inference associated with nfimt 1898. (Contributed by Mario Carneiro, 11-Aug-2016.) (Proof shortened by Wolf Lammen, 2-Jan-2018.) df-nf 1786 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 1898	. 2 ⊢ ((Ⅎ𝑥𝜑 ∧ Ⅎ𝑥𝜓) → Ⅎ𝑥(𝜑 → 𝜓))
4	1, 2, 3	mp2an 690	1 ⊢ Ⅎ𝑥(𝜑 → 𝜓)

Syntax hints:   → wi 4  Ⅎwnf 1785

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

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-nf 1786

This theorem is referenced by:  nfor  1907  nfia1  2150  nfnf1  2151  nfnf  2319  nfsbvOLD  2324  sbievg  2359  mof  2556  cbvmow  2596  moexexlem  2621  nfabdwOLD  2926  cbvralfw  3285  cbvralfwOLD  3302  cbvralf  3331  vtocl2gf  3530  vtocl3gf  3531  vtoclgaf  3534  vtocl2gaf  3537  vtocl3gaf  3538  rspct  3568  rspc  3570  ralab2  3658  mob  3678  reu2eqd  3697  reu8nf  3836  csbhypf  3887  cbvralcsf  3903  dfss2f  3937  rspn0OLD  4318  2reu4lem  4488  reusngf  4638  rexreusng  4645  reuprg0  4668  elintabOLD  4925  axrep2  5250  axrep3  5251  reusv2lem4  5361  reusv3  5365  iunopeqop  5483  nfpo  5555  nffr  5612  reuop  6250  frpoinsg  6302  wfisgOLD  6313  fv3  6865  fvmptss  6965  fvmptd3f  6968  fvmptt  6973  fvmptf  6974  fmptco  7080  dff13f  7208  ovmpos  7508  ov2gf  7509  ovmpodf  7516  ov3  7522  tfisg  7795  tfis  7796  tfinds  7801  tfindes  7804  findes  7844  dfoprab4f  7993  offval22  8025  frpoins3xpg  8077  frpoins3xp3g  8078  tfr3  8350  dom2lem  8939  findcard2  9115  findcard2OLD  9235  ac6sfi  9238  frinsg  9696  dfac8clem  9977  aceq1  10062  dfac5lem5  10072  zfcndrep  10559  zfcndinf  10563  pwfseqlem4a  10606  pwfseqlem4  10607  uzind4s  12842  rabssnn0fi  13901  seqof2  13976  rlim2  15390  ello1mpt  15415  o1compt  15481  summolem2a  15611  sumss  15620  fsumclf  15634  fsumsplitf  15638  fsumsplit1  15641  o1fsum  15709  prodmolem2a  15828  fprodn0  15873  fproddivf  15881  fprodsplitf  15882  fprodsplit1f  15884  prmind2  16572  mreiincl  17490  gsumcom2  19766  gsummptnn0fz  19777  gsummoncoe1  21712  mdetralt2  21995  mdetunilem2  21999  ptcldmpt  23002  cnmptcom  23066  elmptrab  23215  isfildlem  23245  dvmptfsum  25376  dvfsumlem2  25428  dvfsumlem4  25430  dvfsumrlim  25432  dvfsum2  25435  coeeq2  25640  dgrle  25641  rlimcnp  26352  lgamgulmlem2  26416  lgseisenlem2  26761  dchrisumlema  26873  dchrisumlem2  26875  dchrisumlem3  26876  nosupbnd1  27099  nosupbnd2  27101  noinfbnd1  27114  noinfbnd2  27116  mptelee  27907  gropd  28045  grstructd  28046  isch3  30246  atom1d  31358  mo5f  31481  ssiun2sf  31545  iinabrex  31554  ssrelf  31601  fmptcof2  31640  aciunf1lem  31645  nn0min  31786  fsumiunle  31795  esum2dlem  32780  fiunelros  32862  measiun  32906  bnj1385  33533  bnj1468  33547  bnj110  33559  bnj849  33626  bnj900  33630  bnj981  33651  bnj1014  33662  bnj1123  33687  bnj1128  33691  bnj1384  33733  bnj1489  33757  bnj1497  33761  setinds  34439  subtr  34862  subtr2  34863  currysetlem  35489  currysetlem1  35491  mptsnunlem  35882  finxpreclem2  35934  finxpreclem6  35940  ptrest  36150  poimirlem24  36175  poimirlem25  36176  poimirlem26  36177  poimirlem28  36179  fdc1  36278  ac6s6  36704  fsumshftd  37487  cdleme31sn1  38917  cdleme32fva  38973  cdlemk36  39449  fphpd  41197  monotuz  41323  monotoddzz  41325  oddcomabszz  41326  setindtrs  41407  aomclem6  41444  flcidc  41559  rababg  41968  ss2iundf  42053  binomcxplemnotnn0  42758  uzwo4  43383  fiiuncl  43395  disjf1  43523  disjinfi  43534  dmrelrnrel  43568  supxrgere  43688  supxrgelem  43692  supxrge  43693  supxrleubrnmptf  43806  monoordxr  43838  monoord2xr  43840  fsummulc1f  43932  fsumnncl  43933  fsumf1of  43935  fsumiunss  43936  fsumreclf  43937  fsumlessf  43938  fsumsermpt  43940  fmul01  43941  fmuldfeqlem1  43943  fmuldfeq  43944  fmul01lt1lem1  43945  fmul01lt1lem2  43946  fprodexp  43955  fprodabs2  43956  fprodcnlem  43960  climmulf  43965  climexp  43966  climsuse  43969  climrecf  43970  climinff  43972  climaddf  43976  mullimc  43977  idlimc  43987  neglimc  44008  addlimc  44009  0ellimcdiv  44010  limclner  44012  climsubmpt  44021  climreclf  44025  climeldmeqmpt  44029  climfveqmpt  44032  fnlimfvre  44035  climfveqf  44041  climfveqmpt3  44043  climeldmeqf  44044  limsupref  44046  limsupbnd1f  44047  climeqf  44049  climeldmeqmpt3  44050  climinf2  44068  climinf2mpt  44075  climinfmpt  44076  limsupmnf  44082  limsupequz  44084  limsupre2  44086  limsupequzmptf  44092  limsupre3  44094  cncfshift  44235  fprodcncf  44261  dvmptmulf  44298  dvnmptdivc  44299  dvnmul  44304  dvmptfprodlem  44305  dvmptfprod  44306  iblspltprt  44334  stoweidlem3  44364  stoweidlem26  44387  stoweidlem31  44392  stoweidlem34  44395  stoweidlem42  44403  stoweidlem43  44404  stoweidlem48  44409  stoweidlem51  44412  stoweidlem59  44420  fourierdlem86  44553  fourierdlem89  44556  fourierdlem91  44558  fourierdlem112  44579  sge0f1o  44743  sge0lempt  44771  sge0iunmptlemfi  44774  sge0iunmptlemre  44776  sge0fodjrnlem  44777  sge0iunmpt  44779  sge0ltfirpmpt2  44787  sge0isummpt2  44793  sge0xaddlem2  44795  sge0xadd  44796  meadjiun  44827  voliunsge0lem  44833  meaiunincf  44844  meaiuninc3  44846  meaiininc  44848  hoimbl2  45026  vonhoire  45033  vonn0ioo2  45051  vonn0icc2  45053  salpreimagelt  45068  salpreimalegt  45070  salpreimagtge  45086  salpreimaltle  45087  salpreimagtlt  45091  2reu8i  45465  eu2ndop1stv  45477  f1oresf1o2  45643  ichnfimlem  45775  ichreuopeq  45785  reupr  45834  reuopreuprim  45838  2zrngmmgm  46364  nfsetrecs  47251  setrec2fun  47257  pgind  47282