Theorem nfim 1903

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

Syntax hints:   → wi 4  Ⅎwnf 1790

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

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-nf 1791

This theorem is referenced by:  nfor  1911  nfia1  2164  nfnf1  2165  nfnf  2335  cbvsbvf  2371  mof  2567  cbvmow  2607  moexexlem  2630  cbvralfw  3279  cbvralf  3324  vtocl2gf  3515  vtocl3gf  3516  vtoclgaf  3519  vtocl2gaf  3522  vtocl3gaf  3523  rspct  3546  rspc  3548  ralab2  3638  mob  3658  reu2eqd  3677  reu8nf  3809  csbhypf  3859  cbvralcsf  3873  dfssf  3906  2reu4lem  4451  reusngf  4606  rexreusng  4611  reuprg0  4634  axrep2  5202  axrep3  5203  reusv2lem4  5330  reusv3  5334  iunopeqop  5462  iunopeqopOLD  5463  nfpo  5532  nffr  5591  reuop  6244  frpoinsg  6294  fv3  6845  fvmptss  6948  fvmptd3f  6951  fvmptt  6956  fvmptf  6957  fmptco  7071  dff13f  7199  ovmpos  7504  ov2gf  7505  ovmpodf  7512  ov3  7519  tfisg  7794  tfis  7795  tfinds  7800  tfindes  7803  findes  7840  dfoprab4f  7998  offval22  8027  frpoins3xpg  8080  frpoins3xp3g  8081  tfr3  8328  dom2lem  8929  findcard2  9089  ac6sfi  9184  setinds  9661  frinsg  9666  dfac8clem  9945  aceq1  10030  dfac5lem5  10040  zfcndrep  10528  zfcndinf  10532  pwfseqlem4a  10575  pwfseqlem4  10576  uzind4s  12849  rabssnn0fi  13939  seqof2  14013  rlim2  15449  ello1mpt  15474  o1compt  15540  summolem2a  15668  sumss  15677  fsumclf  15691  fsumsplitf  15695  fsumsplit1  15698  o1fsum  15767  prodmolem2a  15890  fprodn0  15935  fproddivf  15943  fprodsplitf  15944  fprodsplit1f  15946  prmind2  16645  mreiincl  17549  gsumcom2  19941  gsummptnn0fz  19952  gsummoncoe1  22294  mdetralt2  22592  mdetunilem2  22596  ptcldmpt  23597  cnmptcom  23661  elmptrab  23810  isfildlem  23840  dvmptfsum  25960  dvfsumlem2  26012  dvfsumlem4  26014  dvfsumrlim  26016  dvfsum2  26019  coeeq2  26225  dgrle  26226  rlimcnp  26947  lgamgulmlem2  27011  lgseisenlem2  27357  dchrisumlema  27469  dchrisumlem2  27471  dchrisumlem3  27472  nosupbnd1  27696  nosupbnd2  27698  noinfbnd1  27711  noinfbnd2  27713  mpteleeOLD  28982  gropd  29118  grstructd  29119  isch3  31330  atom1d  32442  mo5f  32576  ssiun2sf  32648  iinabrex  32658  ssrelf  32707  fmptcof2  32749  aciunf1lem  32754  nn0min  32913  fsumiunle  32921  esum2dlem  34276  fiunelros  34358  measiun  34402  bnj1385  35014  bnj1468  35028  bnj110  35040  bnj849  35107  bnj900  35111  bnj981  35132  bnj1014  35143  bnj1123  35168  bnj1128  35172  bnj1384  35214  bnj1489  35238  bnj1497  35242  subtr  36542  subtr2  36543  regsfromsetind  36767  currysetlem  37298  currysetlem1  37300  mptsnunlem  37700  finxpreclem2  37752  finxpreclem6  37758  ptrest  37986  poimirlem24  38011  poimirlem25  38012  poimirlem26  38013  poimirlem28  38015  fdc1  38113  ac6s6  38539  fsumshftd  39444  cdleme31sn1  40873  cdleme32fva  40929  cdlemk36  41405  eu6w  43126  fphpd  43261  monotuz  43386  monotoddzz  43388  oddcomabszz  43389  setindtrs  43470  aomclem6  43504  flcidc  43615  rababg  44018  ss2iundf  44103  binomcxplemnotnn0  44800  nfrelp  45393  uzwo4  45501  fiiuncl  45513  disjf1  45630  disjinfi  45639  dmrelrnrel  45671  supxrgere  45778  supxrgelem  45782  supxrge  45783  supxrleubrnmptf  45894  monoordxr  45925  monoord2xr  45927  fsummulc1f  46016  fsumnncl  46017  fsumf1of  46019  fsumiunss  46020  fsumreclf  46021  fsumlessf  46022  fsumsermpt  46024  fmul01  46025  fmuldfeqlem1  46027  fmuldfeq  46028  fmul01lt1lem1  46029  fmul01lt1lem2  46030  fprodexp  46039  fprodabs2  46040  fprodcnlem  46044  climmulf  46049  climexp  46050  climsuse  46053  climrecf  46054  climinff  46056  climaddf  46060  mullimc  46061  idlimc  46071  neglimc  46090  addlimc  46091  0ellimcdiv  46092  limclner  46094  climsubmpt  46103  climreclf  46107  climeldmeqmpt  46111  climfveqmpt  46114  fnlimfvre  46117  climfveqf  46123  climfveqmpt3  46125  climeldmeqf  46126  limsupref  46128  limsupbnd1f  46129  climeqf  46131  climeldmeqmpt3  46132  climinf2  46150  climinf2mpt  46157  climinfmpt  46158  limsupmnf  46164  limsupequz  46166  limsupre2  46168  limsupequzmptf  46174  limsupre3  46176  cncfshift  46317  fprodcncf  46343  dvmptmulf  46380  dvnmptdivc  46381  dvnmul  46386  dvmptfprodlem  46387  dvmptfprod  46388  iblspltprt  46416  stoweidlem3  46446  stoweidlem26  46469  stoweidlem31  46474  stoweidlem34  46477  stoweidlem42  46485  stoweidlem43  46486  stoweidlem48  46491  stoweidlem51  46494  stoweidlem59  46502  fourierdlem86  46635  fourierdlem89  46638  fourierdlem91  46640  fourierdlem112  46661  sge0f1o  46825  sge0lempt  46853  sge0iunmptlemfi  46856  sge0iunmptlemre  46858  sge0fodjrnlem  46859  sge0iunmpt  46861  sge0ltfirpmpt2  46869  sge0isummpt2  46875  sge0xaddlem2  46877  sge0xadd  46878  meadjiun  46909  voliunsge0lem  46915  meaiunincf  46926  meaiuninc3  46928  meaiininc  46930  hoimbl2  47108  vonhoire  47115  vonn0ioo2  47133  vonn0icc2  47135  salpreimagelt  47150  salpreimalegt  47152  salpreimagtge  47168  salpreimaltle  47169  salpreimagtlt  47173  2reu8i  47576  eu2ndop1stv  47588  f1oresf1o2  47754  ichnfimlem  47938  ichreuopeq  47948  reupr  47997  reuopreuprim  48001  2zrngmmgm  48743  nfsetrecs  50176  setrec2fun  50182  pgind  50207