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  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  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  5366  reusv3  5370  iunopeqop  5498  iunopeqopOLD  5499  nfpo  5569  nffr  5628  reuop  6291  frpoinsg  6341  fv3  6896  fvmptss  6999  fvmptd3f  7002  fvmptt  7007  fvmptf  7008  fmptco  7123  dff13f  7252  ovmpos  7561  ov2gf  7562  ovmpodf  7569  ov3  7576  tfisg  7850  tfis  7851  tfinds  7856  tfindes  7859  findes  7897  dfoprab4f  8053  offval22  8085  frpoins3xpg  8138  frpoins3xp3g  8139  tfr3  8388  dom2lem  8998  findcard2  9159  ac6sfi  9254  setinds  9728  frinsg  9733  dfac8clem  10035  aceq1  10120  dfac5lem5  10130  zfcndrep  10623  zfcndinf  10627  pwfseqlem4a  10670  pwfseqlem4  10671  uzind4s  12957  rabssnn0fi  14050  seqof2  14124  rlim2  15583  ello1mpt  15608  o1compt  15674  summolem2a  15801  sumss  15810  fsumclf  15824  fsumsplitf  15828  fsumsplit1  15831  o1fsum  15900  prodmolem2a  16021  fprodn0  16066  fproddivf  16074  fprodsplitf  16075  fprodsplit1f  16077  prmind2  16775  mreiincl  17680  gsumcom2  20102  gsummptnn0fz  20113  gsummoncoe1  22533  mdetralt2  22831  mdetunilem2  22835  ptcldmpt  23840  cnmptcom  23904  elmptrab  24053  isfildlem  24083  dvmptfsum  26202  dvfsumlem2  26254  dvfsumlem4  26256  dvfsumrlim  26258  dvfsum2  26261  coeeq2  26468  dgrle  26469  rlimcnp  27202  lgamgulmlem2  27266  lgseisenlem2  27612  dchrisumlema  27724  dchrisumlem2  27726  dchrisumlem3  27727  nosupbnd1  27950  nosupbnd2  27952  noinfbnd1  27965  noinfbnd2  27967  mpteleeOLD  29352  gropd  29488  grstructd  29489  isch3  31722  atom1d  32834  mo5f  32964  ssiun2sf  33033  iinabrex  33042  ssrelf  33088  fmptcof2  33130  aciunf1lem  33135  nn0min  33291  fsumiunle  33299  esum2dlem  34602  fiunelros  34685  measiun  34729  bnj1385  35341  bnj1468  35355  bnj110  35367  bnj849  35434  bnj900  35438  bnj981  35459  bnj1014  35470  bnj1123  35495  bnj1128  35499  bnj1384  35541  bnj1489  35565  bnj1497  35569  subtr  36933  subtr2  36934  regsfromsetind  37158  currysetlem  37689  currysetlem1  37691  mptsnunlem  38092  finxpreclem2  38144  finxpreclem6  38150  ptrest  38368  poimirlem24  38393  poimirlem25  38394  poimirlem26  38395  poimirlem28  38397  fdc1  38496  ac6s6  38920  fsumshftd  39825  cdleme31sn1  41254  cdleme32fva  41310  cdlemk36  41786  eu6w  43522  fphpd  43657  monotuz  43782  monotoddzz  43784  oddcomabszz  43785  setindtrs  43866  aomclem6  43900  flcidc  44011  rababg  44414  ss2iundf  44499  binomcxplemnotnn0  45180  nfrelp  45772  uzwo4  45887  fiiuncl  45899  disjf1  46015  disjinfi  46024  dmrelrnrel  46056  supxrgere  46163  supxrgelem  46167  supxrge  46168  supxrleubrnmptf  46279  monoordxr  46310  monoord2xr  46312  fsummulc1f  46401  fsumnncl  46402  fsumf1of  46404  fsumiunss  46405  fsumreclf  46406  fsumlessf  46407  fsumsermpt  46409  fmul01  46410  fmuldfeqlem1  46412  fmuldfeq  46413  fmul01lt1lem1  46414  fmul01lt1lem2  46415  fprodexp  46424  fprodabs2  46425  fprodcnlem  46429  climmulf  46434  climexp  46435  climsuse  46438  climrecf  46439  climinff  46441  climaddf  46445  mullimc  46446  idlimc  46456  neglimc  46475  addlimc  46476  0ellimcdiv  46477  limclner  46479  climsubmpt  46488  climreclf  46492  climeldmeqmpt  46496  climfveqmpt  46499  fnlimfvre  46502  climfveqf  46508  climfveqmpt3  46510  climeldmeqf  46511  limsupref  46513  limsupbnd1f  46514  climeqf  46516  climeldmeqmpt3  46517  climinf2  46535  climinf2mpt  46542  climinfmpt  46543  limsupmnf  46549  limsupequz  46551  limsupre2  46553  limsupequzmptf  46559  limsupre3  46561  cncfshift  46702  fprodcncf  46728  dvmptmulf  46765  dvnmptdivc  46766  dvnmul  46771  dvmptfprodlem  46772  dvmptfprod  46773  iblspltprt  46801  stoweidlem3  46831  stoweidlem26  46854  stoweidlem31  46859  stoweidlem34  46862  stoweidlem42  46870  stoweidlem43  46871  stoweidlem48  46876  stoweidlem51  46879  stoweidlem59  46887  fourierdlem86  47020  fourierdlem89  47023  fourierdlem91  47025  fourierdlem112  47046  sge0f1o  47210  sge0lempt  47238  sge0iunmptlemfi  47241  sge0iunmptlemre  47243  sge0fodjrnlem  47244  sge0iunmpt  47246  sge0ltfirpmpt2  47254  sge0isummpt2  47260  sge0xaddlem2  47262  sge0xadd  47263  meadjiun  47294  voliunsge0lem  47300  meaiunincf  47311  meaiuninc3  47313  meaiininc  47315  hoimbl2  47493  vonhoire  47500  vonn0ioo2  47518  vonn0icc2  47520  salpreimagelt  47535  salpreimalegt  47537  salpreimagtge  47553  salpreimaltle  47554  salpreimagtlt  47558  2reu8i  48001  eu2ndop1stv  48013  f1oresf1o2  48179  ichnfimlem  48363  ichreuopeq  48373  reupr  48422  reuopreuprim  48426  2zrngmmgm  49167  nfsetrecs  50612  setrec2fun  50618  pgind  50643  nfals  50732  nfrals  50733  nfalseu  50763  nfralseu  50764