Theorem nfim 1929

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

This proof depends on syntax axioms:   → wi 4  Ⅎwnf 1816

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-nf 1817

This theorem is used by:  nfor  1937  nfia1  2190  nfnf1  2191  nfnf  2357  cbvsbvf  2393  mof  2589  cbvmow  2629  moexexlem  2652  cbvralfw  3303  cbvralf  3346  vtocl2gf  3532  vtocl3gf  3533  vtoclgaf  3536  vtocl2gaf  3539  vtocl3gaf  3540  rspct  3563  rspc  3565  ralab2  3655  mob  3675  reu2eqd  3694  reu8nf  3824  csbhypf  3875  cbvralcsf  3889  dfssf  3922  2reu4lem  4479  reusngf  4635  rexreusng  4640  reuprg0  4663  axrep2  5235  axrep3  5236  reusv2lem4  5363  reusv3  5367  iunopeqop  5494  iunopeqopOLD  5495  nfpo  5565  nffr  5624  reuop  6295  frpoinsg  6345  fv3  6901  fvmptss  7004  fvmptd3f  7007  fvmptt  7012  fvmptf  7013  fmptco  7128  dff13f  7257  ovmpos  7566  ov2gf  7567  ovmpodf  7574  ov3  7581  tfisg  7863  tfis  7864  tfinds  7869  tfindes  7872  findes  7910  dfoprab4f  8065  offval22  8097  frpoins3xpg  8150  frpoins3xp3g  8151  tfr3  8400  dom2lem  9012  findcard2  9173  ac6sfi  9268  setinds  9743  frinsg  9748  setrec2fun  9966  dfac8clem  10104  aceq1  10189  dfac5lem5  10199  zfcndrep  10692  zfcndinf  10696  pwfseqlem4a  10739  pwfseqlem4  10740  uzind4s  13028  rabssnn0fi  14122  seqof2  14196  rlim2  15656  ello1mpt  15681  o1compt  15747  summolem2a  15874  sumss  15883  fsumclf  15897  fsumsplitf  15901  fsumsplit1  15904  o1fsum  15973  prodmolem2a  16094  fprodn0  16139  fproddivf  16147  fprodsplitf  16148  fprodsplit1f  16150  prmind2  16853  mreiincl  17759  gsumcom2  20182  gsummptnn0fz  20193  gsummoncoe1  22619  mdetralt2  22917  mdetunilem2  22921  ptcldmpt  23926  cnmptcom  23990  elmptrab  24139  isfildlem  24169  dvmptfsum  26288  dvfsumlem2  26340  dvfsumlem4  26342  dvfsumrlim  26344  dvfsum2  26347  coeeq2  26554  dgrle  26555  rlimcnp  27286  lgamgulmlem2  27350  lgseisenlem2  27696  dchrisumlema  27808  dchrisumlem2  27810  dchrisumlem3  27811  nosupbnd1  28064  nosupbnd2  28066  noinfbnd1  28079  noinfbnd2  28081  mpteleeOLD  29466  gropd  29602  grstructd  29603  isch3  31836  atom1d  32948  mo5f  33078  ssiun2sf  33147  iinabrex  33156  ssrelf  33202  fmptcof2  33244  aciunf1lem  33249  nn0min  33405  fsumiunle  33413  esum2dlem  34717  fiunelros  34800  measiun  34844  bnj1385  35455  bnj1468  35469  bnj110  35481  bnj849  35548  bnj900  35552  bnj981  35573  bnj1014  35584  bnj1123  35609  bnj1128  35613  bnj1384  35655  bnj1489  35679  bnj1497  35683  subtr  37082  subtr2  37083  regsfromsetind  37307  currysetlem  37838  currysetlem1  37840  mptsnunlem  38241  finxpreclem2  38293  finxpreclem6  38299  ptrest  38517  poimirlem24  38542  poimirlem25  38543  poimirlem26  38544  poimirlem28  38546  fdc1  38660  ac6s6  39084  fsumshftd  39989  cdleme31sn1  41418  cdleme32fva  41474  cdlemk36  41950  eu6w  43667  fphpd  43802  monotuz  43927  monotoddzz  43929  oddcomabszz  43930  setindtrs  44011  aomclem6  44045  flcidc  44156  rababg  44559  ss2iundf  44644  binomcxplemnotnn0  45325  nfrelp  45917  uzwo4  46039  fiiuncl  46051  disjf1  46167  disjinfi  46176  dmrelrnrel  46208  supxrgere  46314  supxrgelem  46318  supxrge  46319  supxrleubrnmptf  46430  monoordxr  46461  monoord2xr  46463  fsummulc1f  46552  fsumnncl  46553  fsumf1of  46555  fsumiunss  46556  fsumreclf  46557  fsumlessf  46558  fsumsermpt  46560  fmul01  46561  fmuldfeqlem1  46563  fmuldfeq  46564  fmul01lt1lem1  46565  fmul01lt1lem2  46566  fprodexp  46575  fprodabs2  46576  fprodcnlem  46580  climmulf  46585  climexp  46586  climsuse  46589  climrecf  46590  climinff  46592  climaddf  46596  mullimc  46597  idlimc  46607  neglimc  46626  addlimc  46627  0ellimcdiv  46628  limclner  46630  climsubmpt  46639  climreclf  46643  climeldmeqmpt  46647  climfveqmpt  46650  fnlimfvre  46653  climfveqf  46659  climfveqmpt3  46661  climeldmeqf  46662  limsupref  46664  limsupbnd1f  46665  climeqf  46667  climeldmeqmpt3  46668  climinf2  46686  climinf2mpt  46693  climinfmpt  46694  limsupmnf  46700  limsupequz  46702  limsupre2  46704  limsupequzmptf  46710  limsupre3  46712  cncfshift  46853  fprodcncf  46879  dvmptmulf  46916  dvnmptdivc  46917  dvnmul  46922  dvmptfprodlem  46923  dvmptfprod  46924  iblspltprt  46952  stoweidlem3  46982  stoweidlem26  47005  stoweidlem31  47010  stoweidlem34  47013  stoweidlem42  47021  stoweidlem43  47022  stoweidlem48  47027  stoweidlem51  47030  stoweidlem59  47038  fourierdlem86  47171  fourierdlem89  47174  fourierdlem91  47176  fourierdlem112  47197  sge0f1o  47361  sge0lempt  47389  sge0iunmptlemfi  47392  sge0iunmptlemre  47394  sge0fodjrnlem  47395  sge0iunmpt  47397  sge0ltfirpmpt2  47405  sge0isummpt2  47411  sge0xaddlem2  47413  sge0xadd  47414  meadjiun  47445  voliunsge0lem  47451  meaiunincf  47462  meaiuninc3  47464  meaiininc  47466  hoimbl2  47644  vonhoire  47651  vonn0ioo2  47669  vonn0icc2  47671  salpreimagelt  47686  salpreimalegt  47688  salpreimagtge  47704  salpreimaltle  47705  salpreimagtlt  47709  2reu8i  48152  eu2ndop1stv  48164  f1oresf1o2  48330  ichnfimlem  48514  ichreuopeq  48524  reupr  48573  reuopreuprim  48577  2zrngmmgm  49318  nfsetrecs  50758  pgind  50779  nfals  50868  nfrals  50869  nfalseu  50899  nfralseu  50900