Theorem nfim 1898

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

Syntax hints:   → wi 4  Ⅎwnf 1784

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

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1781  df-nf 1785

This theorem is referenced by:  nfor  1906  nfia1  2149  nfnf1  2150  nfnf  2318  nfsbvOLD  2323  cbvsbvf  2359  mof  2556  cbvmow  2596  moexexlem  2621  nfabdwOLD  2926  cbvralfw  3300  cbvralfwOLD  3319  cbvralf  3355  vtocl2gf  3561  vtocl3gf  3562  vtoclgaf  3565  vtocl2gaf  3568  vtocl3gaf  3569  rspct  3598  rspc  3600  ralab2  3693  mob  3713  reu2eqd  3732  reu8nf  3871  csbhypf  3922  cbvralcsf  3938  dfss2f  3972  rspn0OLD  4353  2reu4lem  4525  reusngf  4676  rexreusng  4683  reuprg0  4706  elintabOLD  4963  axrep2  5288  axrep3  5289  reusv2lem4  5399  reusv3  5403  iunopeqop  5521  nfpo  5593  nffr  5650  reuop  6292  frpoinsg  6344  wfisgOLD  6355  fv3  6909  fvmptss  7010  fvmptd3f  7013  fvmptt  7018  fvmptf  7019  fmptco  7129  dff13f  7258  ovmpos  7559  ov2gf  7560  ovmpodf  7567  ov3  7574  tfisg  7847  tfis  7848  tfinds  7853  tfindes  7856  findes  7897  dfoprab4f  8046  offval22  8078  frpoins3xpg  8130  frpoins3xp3g  8131  tfr3  8403  dom2lem  8992  findcard2  9168  findcard2OLD  9288  ac6sfi  9291  frinsg  9750  dfac8clem  10031  aceq1  10116  dfac5lem5  10126  zfcndrep  10613  zfcndinf  10617  pwfseqlem4a  10660  pwfseqlem4  10661  uzind4s  12897  rabssnn0fi  13956  seqof2  14031  rlim2  15445  ello1mpt  15470  o1compt  15536  summolem2a  15666  sumss  15675  fsumclf  15689  fsumsplitf  15693  fsumsplit1  15696  o1fsum  15764  prodmolem2a  15883  fprodn0  15928  fproddivf  15936  fprodsplitf  15937  fprodsplit1f  15939  prmind2  16627  mreiincl  17545  gsumcom2  19885  gsummptnn0fz  19896  gsummoncoe1  22049  mdetralt2  22332  mdetunilem2  22336  ptcldmpt  23339  cnmptcom  23403  elmptrab  23552  isfildlem  23582  dvmptfsum  25728  dvfsumlem2  25780  dvfsumlem4  25782  dvfsumrlim  25784  dvfsum2  25787  coeeq2  25992  dgrle  25993  rlimcnp  26707  lgamgulmlem2  26771  lgseisenlem2  27116  dchrisumlema  27228  dchrisumlem2  27230  dchrisumlem3  27231  nosupbnd1  27454  nosupbnd2  27456  noinfbnd1  27469  noinfbnd2  27471  mptelee  28421  gropd  28559  grstructd  28560  isch3  30762  atom1d  31874  mo5f  31997  ssiun2sf  32059  iinabrex  32068  ssrelf  32112  fmptcof2  32150  aciunf1lem  32155  nn0min  32294  fsumiunle  32303  esum2dlem  33389  fiunelros  33471  measiun  33515  bnj1385  34142  bnj1468  34156  bnj110  34168  bnj849  34235  bnj900  34239  bnj981  34260  bnj1014  34271  bnj1123  34296  bnj1128  34300  bnj1384  34342  bnj1489  34366  bnj1497  34370  setinds  35055  gg-dvfsumlem2  35470  subtr  35503  subtr2  35504  currysetlem  36130  currysetlem1  36132  mptsnunlem  36523  finxpreclem2  36575  finxpreclem6  36581  ptrest  36791  poimirlem24  36816  poimirlem25  36817  poimirlem26  36818  poimirlem28  36820  fdc1  36918  ac6s6  37344  fsumshftd  38126  cdleme31sn1  39556  cdleme32fva  39612  cdlemk36  40088  fphpd  41857  monotuz  41983  monotoddzz  41985  oddcomabszz  41986  setindtrs  42067  aomclem6  42104  flcidc  42219  rababg  42628  ss2iundf  42713  binomcxplemnotnn0  43418  uzwo4  44042  fiiuncl  44054  disjf1  44181  disjinfi  44190  dmrelrnrel  44224  supxrgere  44342  supxrgelem  44346  supxrge  44347  supxrleubrnmptf  44460  monoordxr  44492  monoord2xr  44494  fsummulc1f  44586  fsumnncl  44587  fsumf1of  44589  fsumiunss  44590  fsumreclf  44591  fsumlessf  44592  fsumsermpt  44594  fmul01  44595  fmuldfeqlem1  44597  fmuldfeq  44598  fmul01lt1lem1  44599  fmul01lt1lem2  44600  fprodexp  44609  fprodabs2  44610  fprodcnlem  44614  climmulf  44619  climexp  44620  climsuse  44623  climrecf  44624  climinff  44626  climaddf  44630  mullimc  44631  idlimc  44641  neglimc  44662  addlimc  44663  0ellimcdiv  44664  limclner  44666  climsubmpt  44675  climreclf  44679  climeldmeqmpt  44683  climfveqmpt  44686  fnlimfvre  44689  climfveqf  44695  climfveqmpt3  44697  climeldmeqf  44698  limsupref  44700  limsupbnd1f  44701  climeqf  44703  climeldmeqmpt3  44704  climinf2  44722  climinf2mpt  44729  climinfmpt  44730  limsupmnf  44736  limsupequz  44738  limsupre2  44740  limsupequzmptf  44746  limsupre3  44748  cncfshift  44889  fprodcncf  44915  dvmptmulf  44952  dvnmptdivc  44953  dvnmul  44958  dvmptfprodlem  44959  dvmptfprod  44960  iblspltprt  44988  stoweidlem3  45018  stoweidlem26  45041  stoweidlem31  45046  stoweidlem34  45049  stoweidlem42  45057  stoweidlem43  45058  stoweidlem48  45063  stoweidlem51  45066  stoweidlem59  45074  fourierdlem86  45207  fourierdlem89  45210  fourierdlem91  45212  fourierdlem112  45233  sge0f1o  45397  sge0lempt  45425  sge0iunmptlemfi  45428  sge0iunmptlemre  45430  sge0fodjrnlem  45431  sge0iunmpt  45433  sge0ltfirpmpt2  45441  sge0isummpt2  45447  sge0xaddlem2  45449  sge0xadd  45450  meadjiun  45481  voliunsge0lem  45487  meaiunincf  45498  meaiuninc3  45500  meaiininc  45502  hoimbl2  45680  vonhoire  45687  vonn0ioo2  45705  vonn0icc2  45707  salpreimagelt  45722  salpreimalegt  45724  salpreimagtge  45740  salpreimaltle  45741  salpreimagtlt  45745  2reu8i  46120  eu2ndop1stv  46132  f1oresf1o2  46298  ichnfimlem  46430  ichreuopeq  46440  reupr  46489  reuopreuprim  46493  2zrngmmgm  46933  nfsetrecs  47819  setrec2fun  47825  pgind  47850