Theorem nfim 1896

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

Syntax hints:   → wi 4  Ⅎwnf 1783

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

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-nf 1784

This theorem is referenced by:  nfor  1904  nfia1  2154  nfnf1  2155  nfnf  2327  cbvsbvf  2366  mof  2563  cbvmow  2603  moexexlem  2626  cbvralfw  3288  cbvralf  3344  vtocl2gf  3556  vtocl3gf  3557  vtoclgaf  3560  vtocl2gaf  3563  vtocl2gafOLD  3564  vtocl3gaf  3565  vtocl3gafOLD  3566  rspct  3592  rspc  3594  ralab2  3685  mob  3705  reu2eqd  3724  reu8nf  3857  csbhypf  3907  cbvralcsf  3921  dfssf  3954  2reu4lem  4502  reusngf  4655  rexreusng  4660  reuprg0  4683  elintabOLD  4940  axrep2  5257  axrep3  5258  reusv2lem4  5376  reusv3  5380  iunopeqop  5501  nfpo  5572  nffr  5632  reuop  6287  frpoinsg  6337  wfisgOLD  6348  fv3  6899  fvmptss  7003  fvmptd3f  7006  fvmptt  7011  fvmptf  7012  fmptco  7124  dff13f  7253  ovmpos  7560  ov2gf  7561  ovmpodf  7568  ov3  7575  tfisg  7854  tfis  7855  tfinds  7860  tfindes  7863  findes  7901  dfoprab4f  8060  offval22  8092  frpoins3xpg  8144  frpoins3xp3g  8145  tfr3  8418  dom2lem  9011  findcard2  9183  ac6sfi  9297  frinsg  9770  dfac8clem  10051  aceq1  10136  dfac5lem5  10146  zfcndrep  10633  zfcndinf  10637  pwfseqlem4a  10680  pwfseqlem4  10681  uzind4s  12929  rabssnn0fi  14009  seqof2  14083  rlim2  15517  ello1mpt  15542  o1compt  15608  summolem2a  15736  sumss  15745  fsumclf  15759  fsumsplitf  15763  fsumsplit1  15766  o1fsum  15834  prodmolem2a  15955  fprodn0  16000  fproddivf  16008  fprodsplitf  16009  fprodsplit1f  16011  prmind2  16709  mreiincl  17613  gsumcom2  19961  gsummptnn0fz  19972  gsummoncoe1  22251  mdetralt2  22552  mdetunilem2  22556  ptcldmpt  23557  cnmptcom  23621  elmptrab  23770  isfildlem  23800  dvmptfsum  25936  dvfsumlem2  25990  dvfsumlem2OLD  25991  dvfsumlem4  25993  dvfsumrlim  25995  dvfsum2  25998  coeeq2  26204  dgrle  26205  rlimcnp  26932  lgamgulmlem2  26997  lgseisenlem2  27344  dchrisumlema  27456  dchrisumlem2  27458  dchrisumlem3  27459  nosupbnd1  27683  nosupbnd2  27685  noinfbnd1  27698  noinfbnd2  27700  mptelee  28879  gropd  29015  grstructd  29016  isch3  31227  atom1d  32339  mo5f  32475  ssiun2sf  32545  iinabrex  32555  ssrelf  32600  fmptcof2  32640  aciunf1lem  32645  nn0min  32804  fsumiunle  32813  esum2dlem  34128  fiunelros  34210  measiun  34254  bnj1385  34868  bnj1468  34882  bnj110  34894  bnj849  34961  bnj900  34965  bnj981  34986  bnj1014  34997  bnj1123  35022  bnj1128  35026  bnj1384  35068  bnj1489  35092  bnj1497  35096  setinds  35801  subtr  36337  subtr2  36338  currysetlem  36968  currysetlem1  36970  mptsnunlem  37361  finxpreclem2  37413  finxpreclem6  37419  ptrest  37648  poimirlem24  37673  poimirlem25  37674  poimirlem26  37675  poimirlem28  37677  fdc1  37775  ac6s6  38201  fsumshftd  38975  cdleme31sn1  40405  cdleme32fva  40461  cdlemk36  40937  eu6w  42674  fphpd  42814  monotuz  42940  monotoddzz  42942  oddcomabszz  42943  setindtrs  43024  aomclem6  43058  flcidc  43169  rababg  43573  ss2iundf  43658  binomcxplemnotnn0  44355  nfrelp  44949  uzwo4  45057  fiiuncl  45069  disjf1  45187  disjinfi  45196  dmrelrnrel  45230  supxrgere  45340  supxrgelem  45344  supxrge  45345  supxrleubrnmptf  45458  monoordxr  45489  monoord2xr  45491  fsummulc1f  45580  fsumnncl  45581  fsumf1of  45583  fsumiunss  45584  fsumreclf  45585  fsumlessf  45586  fsumsermpt  45588  fmul01  45589  fmuldfeqlem1  45591  fmuldfeq  45592  fmul01lt1lem1  45593  fmul01lt1lem2  45594  fprodexp  45603  fprodabs2  45604  fprodcnlem  45608  climmulf  45613  climexp  45614  climsuse  45617  climrecf  45618  climinff  45620  climaddf  45624  mullimc  45625  idlimc  45635  neglimc  45656  addlimc  45657  0ellimcdiv  45658  limclner  45660  climsubmpt  45669  climreclf  45673  climeldmeqmpt  45677  climfveqmpt  45680  fnlimfvre  45683  climfveqf  45689  climfveqmpt3  45691  climeldmeqf  45692  limsupref  45694  limsupbnd1f  45695  climeqf  45697  climeldmeqmpt3  45698  climinf2  45716  climinf2mpt  45723  climinfmpt  45724  limsupmnf  45730  limsupequz  45732  limsupre2  45734  limsupequzmptf  45740  limsupre3  45742  cncfshift  45883  fprodcncf  45909  dvmptmulf  45946  dvnmptdivc  45947  dvnmul  45952  dvmptfprodlem  45953  dvmptfprod  45954  iblspltprt  45982  stoweidlem3  46012  stoweidlem26  46035  stoweidlem31  46040  stoweidlem34  46043  stoweidlem42  46051  stoweidlem43  46052  stoweidlem48  46057  stoweidlem51  46060  stoweidlem59  46068  fourierdlem86  46201  fourierdlem89  46204  fourierdlem91  46206  fourierdlem112  46227  sge0f1o  46391  sge0lempt  46419  sge0iunmptlemfi  46422  sge0iunmptlemre  46424  sge0fodjrnlem  46425  sge0iunmpt  46427  sge0ltfirpmpt2  46435  sge0isummpt2  46441  sge0xaddlem2  46443  sge0xadd  46444  meadjiun  46475  voliunsge0lem  46481  meaiunincf  46492  meaiuninc3  46494  meaiininc  46496  hoimbl2  46674  vonhoire  46681  vonn0ioo2  46699  vonn0icc2  46701  salpreimagelt  46716  salpreimalegt  46718  salpreimagtge  46734  salpreimaltle  46735  salpreimagtlt  46739  2reu8i  47122  eu2ndop1stv  47134  f1oresf1o2  47300  ichnfimlem  47457  ichreuopeq  47467  reupr  47516  reuopreuprim  47520  2zrngmmgm  48207  nfsetrecs  49530  setrec2fun  49536  pgind  49561