Theorem nfim 1897

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

Syntax hints:   → wi 4  Ⅎwnf 1784

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

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-nf 1785

This theorem is referenced by:  nfor  1905  nfia1  2157  nfnf1  2158  nfnf  2345  nfsbv  2349  nfsbvOLD  2350  cbval2vOLD  2364  cbval2OLD  2433  mof  2647  moexexlem  2711  nfabdw  3002  cbvralfw  3439  cbvralf  3441  vtocl2gf  3572  vtocl3gf  3573  vtoclgaf  3575  vtocl2gaf  3578  vtocl3gaf  3579  rspct  3611  rspc  3613  ralab2  3690  ralab2OLD  3691  mob  3710  reu2eqd  3729  reu8nf  3862  csbhypf  3913  cbvralcsf  3927  vtocl2dOLD  3933  dfss2f  3960  rspn0  4315  2reu4lem  4467  reusngf  4614  rexreusng  4619  reuprg0  4640  elintab  4889  axrep2  5195  axrep3  5196  reusv2lem4  5304  reusv3  5308  iunopeqop  5413  nfpo  5481  nffr  5531  reuop  6146  wfisg  6185  fv3  6690  fvmptss  6782  fvmptd3f  6785  fvmptt  6790  fvmptf  6791  fmptco  6893  dff13f  7016  ovmpos  7300  ov2gf  7301  ovmpodf  7308  ov3  7313  tfis  7571  tfinds  7576  tfindes  7579  findes  7614  dfoprab4f  7756  offval22  7785  tfr3  8037  dom2lem  8551  findcard2  8760  ac6sfi  8764  dfac8clem  9460  aceq1  9545  dfac5lem5  9555  zfcndrep  10038  zfcndinf  10042  pwfseqlem4a  10085  pwfseqlem4  10086  uzind4s  12311  rabssnn0fi  13357  seqof2  13431  rlim2  14855  ello1mpt  14880  o1compt  14946  summolem2a  15074  sumss  15083  fsumsplitf  15100  o1fsum  15170  prodmolem2a  15290  fprodn0  15335  fproddivf  15343  fprodsplitf  15344  fprodsplit1f  15346  prmind2  16031  mreiincl  16869  gsumcom2  19097  gsummptnn0fz  19108  gsummoncoe1  20474  mdetralt2  21220  mdetunilem2  21224  ptcldmpt  22224  cnmptcom  22288  elmptrab  22437  isfildlem  22467  dvmptfsum  24574  dvfsumlem2  24626  dvfsumlem4  24628  dvfsumrlim  24630  dvfsum2  24633  coeeq2  24834  dgrle  24835  rlimcnp  25545  lgamgulmlem2  25609  lgseisenlem2  25954  dchrisumlema  26066  dchrisumlem2  26068  dchrisumlem3  26069  mptelee  26683  gropd  26818  grstructd  26819  isch3  29020  atom1d  30132  mo5f  30255  ssiun2sf  30313  ssrelf  30368  fmptcof2  30404  aciunf1lem  30409  nn0min  30538  fsumiunle  30547  esum2dlem  31353  fiunelros  31435  measiun  31479  bnj1385  32106  bnj1468  32120  bnj110  32132  bnj849  32199  bnj900  32203  bnj981  32224  bnj1014  32235  bnj1123  32260  bnj1128  32264  bnj1384  32306  bnj1489  32330  bnj1497  32334  setinds  33025  tfisg  33057  frpoinsg  33083  frinsg  33089  nosupbnd1  33216  nosupbnd2  33218  subtr  33664  subtr2  33665  currysetlem  34258  currysetlem1  34260  mptsnunlem  34621  finxpreclem2  34673  finxpreclem6  34679  ptrest  34893  poimirlem24  34918  poimirlem25  34919  poimirlem26  34920  poimirlem28  34922  fdc1  35023  ac6s6  35452  fsumshftd  36090  cdleme31sn1  37519  cdleme32fva  37575  cdlemk36  38051  fphpd  39420  monotuz  39545  monotoddzz  39547  oddcomabszz  39548  setindtrs  39629  aomclem6  39666  flcidc  39781  rababg  39940  ss2iundf  40011  binomcxplemnotnn0  40695  uzwo4  41322  fiiuncl  41334  disjf1  41450  disjinfi  41461  dmrelrnrel  41497  supxrgere  41608  supxrgelem  41612  supxrge  41613  supxrleubrnmptf  41734  monoordxr  41766  monoord2xr  41768  fsumclf  41857  fsummulc1f  41858  fsumnncl  41859  fsumsplit1  41860  fsumf1of  41862  fsumiunss  41863  fsumreclf  41864  fsumlessf  41865  fsumsermpt  41867  fmul01  41868  fmuldfeqlem1  41870  fmuldfeq  41871  fmul01lt1lem1  41872  fmul01lt1lem2  41873  fprodexp  41882  fprodabs2  41883  fprodcnlem  41887  climmulf  41892  climexp  41893  climsuse  41896  climrecf  41897  climinff  41899  climaddf  41903  mullimc  41904  idlimc  41914  neglimc  41935  addlimc  41936  0ellimcdiv  41937  limclner  41939  climsubmpt  41948  climreclf  41952  climeldmeqmpt  41956  climfveqmpt  41959  fnlimfvre  41962  climfveqf  41968  climfveqmpt3  41970  climeldmeqf  41971  limsupref  41973  limsupbnd1f  41974  climeqf  41976  climeldmeqmpt3  41977  climinf2  41995  climinf2mpt  42002  climinfmpt  42003  limsupmnf  42009  limsupequz  42011  limsupre2  42013  limsupequzmptf  42019  limsupre3  42021  cncfshift  42164  fprodcncf  42191  dvmptmulf  42229  dvnmptdivc  42230  dvnmul  42235  dvmptfprodlem  42236  dvmptfprod  42237  iblspltprt  42265  stoweidlem3  42295  stoweidlem26  42318  stoweidlem31  42323  stoweidlem34  42326  stoweidlem42  42334  stoweidlem43  42335  stoweidlem48  42340  stoweidlem51  42343  stoweidlem59  42351  fourierdlem86  42484  fourierdlem89  42487  fourierdlem91  42489  fourierdlem112  42510  sge0f1o  42671  sge0lempt  42699  sge0iunmptlemfi  42702  sge0iunmptlemre  42704  sge0fodjrnlem  42705  sge0iunmpt  42707  sge0ltfirpmpt2  42715  sge0isummpt2  42721  sge0xaddlem2  42723  sge0xadd  42724  meadjiun  42755  voliunsge0lem  42761  meaiunincf  42772  meaiuninc3  42774  meaiininc  42776  hoimbl2  42954  vonhoire  42961  vonn0ioo2  42979  vonn0icc2  42981  salpreimagelt  42993  salpreimalegt  42995  salpreimagtge  43009  salpreimaltle  43010  salpreimagtlt  43014  2reu8i  43319  eu2ndop1stv  43331  f1oresf1o2  43497  ichreuopeq  43642  reupr  43691  reuopreuprim  43695  2zrngmmgm  44224  nfsetrecs  44796  setrec2fun  44802