Theorem nfim 1928

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

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

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

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-nf 1816

This theorem is used by:  nfor  1936  nfia1  2189  nfnf1  2190  nfnf  2356  cbvsbvf  2392  mof  2588  cbvmow  2628  moexexlem  2651  cbvralfw  3302  cbvralf  3345  vtocl2gf  3531  vtocl3gf  3532  vtoclgaf  3535  vtocl2gaf  3538  vtocl3gaf  3539  rspct  3562  rspc  3564  ralab2  3654  mob  3674  reu2eqd  3693  reu8nf  3824  csbhypf  3875  cbvralcsf  3889  dfssf  3900  2reu4lem  4478  reusngf  4631  rexreusng  4636  reuprg0  4659  axrep2  5234  axrep3  5235  reusv2lem4  5363  reusv3  5367  iunopeqop  5494  iunopeqopOLD  5495  nfpo  5565  nffr  5624  reuop  6299  frpoinsg  6349  fv3  6908  fvmptss  7011  fvmptd3f  7014  fvmptt  7019  fvmptf  7020  fmptco  7135  dff13f  7263  ovmpos  7572  ov2gf  7573  ovmpodf  7580  ov3  7587  tfisg  7869  tfis  7870  tfinds  7875  tfindes  7878  findes  7916  dfoprab4f  8071  offval22  8103  frpoins3xpg  8163  frpoins3xp3g  8164  tfr3  8414  dom2lem  9026  findcard2  9187  ac6sfi  9282  setinds  9757  frinsg  9762  setrec2fun  9980  dfac8clem  10118  aceq1  10203  dfac5lem5  10213  zfcndrep  10706  zfcndinf  10710  pwfseqlem4a  10753  pwfseqlem4  10754  uzind4s  13042  rabssnn0fi  14136  seqof2  14210  rlim2  15672  ello1mpt  15697  o1compt  15763  summolem2a  15890  sumss  15899  fsumclf  15913  fsumsplitf  15917  fsumsplit1  15920  o1fsum  15989  prodmolem2a  16110  fprodn0  16155  fproddivf  16163  fprodsplitf  16164  fprodsplit1f  16166  prmind2  16869  mreiincl  17775  gsumcom2  20198  gsummptnn0fz  20209  gsummoncoe1  22635  mdetralt2  22933  mdetunilem2  22937  ptcldmpt  23942  cnmptcom  24006  elmptrab  24155  isfildlem  24185  dvmptfsum  26304  dvfsumlem2  26356  dvfsumlem4  26358  dvfsumrlim  26360  dvfsum2  26363  coeeq2  26570  dgrle  26571  rlimcnp  27302  lgamgulmlem2  27366  lgseisenlem2  27712  dchrisumlema  27824  dchrisumlem2  27826  dchrisumlem3  27827  nosupbnd1  28080  nosupbnd2  28082  noinfbnd1  28095  noinfbnd2  28097  mpteleeOLD  29482  gropd  29618  grstructd  29619  isch3  31852  atom1d  32964  mo5f  33136  ssiun2sf  33205  iinabrex  33214  ssrelf  33260  fmptcof2  33302  aciunf1lem  33307  nn0min  33462  fsumiunle  33470  esum2dlem  34774  fiunelros  34857  measiun  34901  bnj1385  35512  bnj1468  35526  bnj110  35538  bnj849  35605  bnj900  35609  bnj981  35630  bnj1014  35641  bnj1123  35666  bnj1128  35670  bnj1384  35712  bnj1489  35736  bnj1497  35740  subtr  37198  subtr2  37199  regsfromsetind  37423  currysetlem  37954  currysetlem1  37956  mptsnunlem  38370  finxpreclem2  38422  finxpreclem6  38428  ptrest  38646  poimirlem24  38671  poimirlem25  38672  poimirlem26  38673  poimirlem28  38675  fdc1  38789  ac6s6  39213  fsumshftd  40118  cdleme31sn1  41547  cdleme32fva  41603  cdlemk36  42079  eu6w  43796  fphpd  43932  monotuz  44057  monotoddzz  44059  oddcomabszz  44060  setindtrs  44141  aomclem6  44170  flcidc  44281  rababg  44684  ss2iundf  44768  binomcxplemnotnn0  45449  nfrelp  46047  uzwo4  46178  fiiuncl  46190  disjf1  46306  disjinfi  46315  dmrelrnrel  46347  supxrgere  46453  supxrgelem  46457  supxrge  46458  supxrleubrnmptf  46569  monoordxr  46600  monoord2xr  46602  fsummulc1f  46691  fsumnncl  46692  fsumf1of  46694  fsumiunss  46695  fsumreclf  46696  fsumlessf  46697  fsumsermpt  46699  fmul01  46700  fmuldfeqlem1  46702  fmuldfeq  46703  fmul01lt1lem1  46704  fmul01lt1lem2  46705  fprodexp  46714  fprodabs2  46715  fprodcnlem  46719  climmulf  46724  climexp  46725  climsuse  46728  climrecf  46729  climinff  46731  climaddf  46735  mullimc  46736  idlimc  46746  neglimc  46765  addlimc  46766  0ellimcdiv  46767  limclner  46769  climsubmpt  46778  climreclf  46782  climeldmeqmpt  46786  climfveqmpt  46789  fnlimfvre  46792  climfveqf  46798  climfveqmpt3  46800  climeldmeqf  46801  limsupref  46803  limsupbnd1f  46804  climeqf  46806  climeldmeqmpt3  46807  climinf2  46825  climinf2mpt  46832  climinfmpt  46833  limsupmnf  46839  limsupequz  46841  limsupre2  46843  limsupequzmptf  46849  limsupre3  46851  cncfshift  46992  fprodcncf  47018  dvmptmulf  47055  dvnmptdivc  47056  dvnmul  47061  dvmptfprodlem  47062  dvmptfprod  47063  iblspltprt  47091  stoweidlem3  47121  stoweidlem26  47144  stoweidlem31  47149  stoweidlem34  47152  stoweidlem42  47160  stoweidlem43  47161  stoweidlem48  47166  stoweidlem51  47169  stoweidlem59  47177  fourierdlem86  47310  fourierdlem89  47313  fourierdlem91  47315  fourierdlem112  47336  sge0f1o  47500  sge0lempt  47528  sge0iunmptlemfi  47531  sge0iunmptlemre  47533  sge0fodjrnlem  47534  sge0iunmpt  47536  sge0ltfirpmpt2  47544  sge0isummpt2  47550  sge0xaddlem2  47552  sge0xadd  47553  meadjiun  47584  voliunsge0lem  47590  meaiunincf  47601  meaiuninc3  47603  meaiininc  47605  hoimbl2  47783  vonhoire  47790  vonn0ioo2  47808  vonn0icc2  47810  salpreimagelt  47825  salpreimalegt  47827  salpreimagtge  47843  salpreimaltle  47844  salpreimagtlt  47848  2reu8i  48292  eu2ndop1stv  48303  f1oresf1o2  48469  ichnfimlem  48653  ichreuopeq  48663  reupr  48712  reuopreuprim  48716  2zrngmmgm  49457  nfsetrecs  50972  pgind  50993  nfals  51082  nfrals  51083  nfalseu  51113  nfralseu  51114