Theorem nfim 1900

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

Syntax hints:   → wi 4  Ⅎwnf 1786

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

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-nf 1787

This theorem is referenced by:  nfor  1908  nfia1  2151  nfnf1  2152  nfnf  2320  nfsbvOLD  2325  cbvsbvf  2361  mof  2558  cbvmow  2598  moexexlem  2623  nfabdwOLD  2928  cbvralfw  3302  cbvralfwOLD  3321  cbvralf  3357  vtocl2gf  3561  vtocl3gf  3562  vtoclgaf  3565  vtocl2gaf  3568  vtocl3gaf  3569  rspct  3599  rspc  3601  ralab2  3694  mob  3714  reu2eqd  3733  reu8nf  3872  csbhypf  3923  cbvralcsf  3939  dfss2f  3973  rspn0OLD  4354  2reu4lem  4526  reusngf  4677  rexreusng  4684  reuprg0  4707  elintabOLD  4964  axrep2  5289  axrep3  5290  reusv2lem4  5400  reusv3  5404  iunopeqop  5522  nfpo  5594  nffr  5651  reuop  6293  frpoinsg  6345  wfisgOLD  6356  fv3  6910  fvmptss  7011  fvmptd3f  7014  fvmptt  7019  fvmptf  7020  fmptco  7127  dff13f  7255  ovmpos  7556  ov2gf  7557  ovmpodf  7564  ov3  7570  tfisg  7843  tfis  7844  tfinds  7849  tfindes  7852  findes  7893  dfoprab4f  8042  offval22  8074  frpoins3xpg  8126  frpoins3xp3g  8127  tfr3  8399  dom2lem  8988  findcard2  9164  findcard2OLD  9284  ac6sfi  9287  frinsg  9746  dfac8clem  10027  aceq1  10112  dfac5lem5  10122  zfcndrep  10609  zfcndinf  10613  pwfseqlem4a  10656  pwfseqlem4  10657  uzind4s  12892  rabssnn0fi  13951  seqof2  14026  rlim2  15440  ello1mpt  15465  o1compt  15531  summolem2a  15661  sumss  15670  fsumclf  15684  fsumsplitf  15688  fsumsplit1  15691  o1fsum  15759  prodmolem2a  15878  fprodn0  15923  fproddivf  15931  fprodsplitf  15932  fprodsplit1f  15934  prmind2  16622  mreiincl  17540  gsumcom2  19843  gsummptnn0fz  19854  gsummoncoe1  21828  mdetralt2  22111  mdetunilem2  22115  ptcldmpt  23118  cnmptcom  23182  elmptrab  23331  isfildlem  23361  dvmptfsum  25492  dvfsumlem2  25544  dvfsumlem4  25546  dvfsumrlim  25548  dvfsum2  25551  coeeq2  25756  dgrle  25757  rlimcnp  26470  lgamgulmlem2  26534  lgseisenlem2  26879  dchrisumlema  26991  dchrisumlem2  26993  dchrisumlem3  26994  nosupbnd1  27217  nosupbnd2  27219  noinfbnd1  27232  noinfbnd2  27234  mptelee  28153  gropd  28291  grstructd  28292  isch3  30494  atom1d  31606  mo5f  31729  ssiun2sf  31791  iinabrex  31800  ssrelf  31844  fmptcof2  31882  aciunf1lem  31887  nn0min  32026  fsumiunle  32035  esum2dlem  33090  fiunelros  33172  measiun  33216  bnj1385  33843  bnj1468  33857  bnj110  33869  bnj849  33936  bnj900  33940  bnj981  33961  bnj1014  33972  bnj1123  33997  bnj1128  34001  bnj1384  34043  bnj1489  34067  bnj1497  34071  setinds  34750  gg-dvfsumlem2  35183  subtr  35199  subtr2  35200  currysetlem  35826  currysetlem1  35828  mptsnunlem  36219  finxpreclem2  36271  finxpreclem6  36277  ptrest  36487  poimirlem24  36512  poimirlem25  36513  poimirlem26  36514  poimirlem28  36516  fdc1  36614  ac6s6  37040  fsumshftd  37822  cdleme31sn1  39252  cdleme32fva  39308  cdlemk36  39784  fphpd  41554  monotuz  41680  monotoddzz  41682  oddcomabszz  41683  setindtrs  41764  aomclem6  41801  flcidc  41916  rababg  42325  ss2iundf  42410  binomcxplemnotnn0  43115  uzwo4  43740  fiiuncl  43752  disjf1  43880  disjinfi  43891  dmrelrnrel  43925  supxrgere  44043  supxrgelem  44047  supxrge  44048  supxrleubrnmptf  44161  monoordxr  44193  monoord2xr  44195  fsummulc1f  44287  fsumnncl  44288  fsumf1of  44290  fsumiunss  44291  fsumreclf  44292  fsumlessf  44293  fsumsermpt  44295  fmul01  44296  fmuldfeqlem1  44298  fmuldfeq  44299  fmul01lt1lem1  44300  fmul01lt1lem2  44301  fprodexp  44310  fprodabs2  44311  fprodcnlem  44315  climmulf  44320  climexp  44321  climsuse  44324  climrecf  44325  climinff  44327  climaddf  44331  mullimc  44332  idlimc  44342  neglimc  44363  addlimc  44364  0ellimcdiv  44365  limclner  44367  climsubmpt  44376  climreclf  44380  climeldmeqmpt  44384  climfveqmpt  44387  fnlimfvre  44390  climfveqf  44396  climfveqmpt3  44398  climeldmeqf  44399  limsupref  44401  limsupbnd1f  44402  climeqf  44404  climeldmeqmpt3  44405  climinf2  44423  climinf2mpt  44430  climinfmpt  44431  limsupmnf  44437  limsupequz  44439  limsupre2  44441  limsupequzmptf  44447  limsupre3  44449  cncfshift  44590  fprodcncf  44616  dvmptmulf  44653  dvnmptdivc  44654  dvnmul  44659  dvmptfprodlem  44660  dvmptfprod  44661  iblspltprt  44689  stoweidlem3  44719  stoweidlem26  44742  stoweidlem31  44747  stoweidlem34  44750  stoweidlem42  44758  stoweidlem43  44759  stoweidlem48  44764  stoweidlem51  44767  stoweidlem59  44775  fourierdlem86  44908  fourierdlem89  44911  fourierdlem91  44913  fourierdlem112  44934  sge0f1o  45098  sge0lempt  45126  sge0iunmptlemfi  45129  sge0iunmptlemre  45131  sge0fodjrnlem  45132  sge0iunmpt  45134  sge0ltfirpmpt2  45142  sge0isummpt2  45148  sge0xaddlem2  45150  sge0xadd  45151  meadjiun  45182  voliunsge0lem  45188  meaiunincf  45199  meaiuninc3  45201  meaiininc  45203  hoimbl2  45381  vonhoire  45388  vonn0ioo2  45406  vonn0icc2  45408  salpreimagelt  45423  salpreimalegt  45425  salpreimagtge  45441  salpreimaltle  45442  salpreimagtlt  45446  2reu8i  45821  eu2ndop1stv  45833  f1oresf1o2  45999  ichnfimlem  46131  ichreuopeq  46141  reupr  46190  reuopreuprim  46194  2zrngmmgm  46844  nfsetrecs  47731  setrec2fun  47737  pgind  47762