Theorem nfim 1898

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

Syntax hints:   → wi 4  Ⅎwnf 1785

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

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-nf 1786

This theorem is referenced by:  nfor  1906  nfia1  2159  nfnf1  2160  nfnf  2331  cbvsbvf  2367  mof  2563  cbvmow  2603  moexexlem  2626  cbvralfw  3277  cbvralf  3322  vtocl2gf  3515  vtocl3gf  3516  vtoclgaf  3519  vtocl2gaf  3522  vtocl2gafOLD  3523  vtocl3gaf  3524  vtocl3gafOLD  3525  rspct  3550  rspc  3552  ralab2  3643  mob  3663  reu2eqd  3682  reu8nf  3815  csbhypf  3865  cbvralcsf  3879  dfssf  3912  2reu4lem  4463  reusngf  4618  rexreusng  4623  reuprg0  4646  axrep2  5215  axrep3  5216  reusv2lem4  5343  reusv3  5347  iunopeqop  5475  iunopeqopOLD  5476  nfpo  5545  nffr  5604  reuop  6257  frpoinsg  6307  fv3  6858  fvmptss  6960  fvmptd3f  6963  fvmptt  6968  fvmptf  6969  fmptco  7082  dff13f  7210  ovmpos  7515  ov2gf  7516  ovmpodf  7523  ov3  7530  tfisg  7805  tfis  7806  tfinds  7811  tfindes  7814  findes  7851  dfoprab4f  8009  offval22  8038  frpoins3xpg  8090  frpoins3xp3g  8091  tfr3  8338  dom2lem  8939  findcard2  9099  ac6sfi  9194  setinds  9670  frinsg  9675  dfac8clem  9954  aceq1  10039  dfac5lem5  10049  zfcndrep  10537  zfcndinf  10541  pwfseqlem4a  10584  pwfseqlem4  10585  uzind4s  12858  rabssnn0fi  13948  seqof2  14022  rlim2  15458  ello1mpt  15483  o1compt  15549  summolem2a  15677  sumss  15686  fsumclf  15700  fsumsplitf  15704  fsumsplit1  15707  o1fsum  15776  prodmolem2a  15899  fprodn0  15944  fproddivf  15952  fprodsplitf  15953  fprodsplit1f  15955  prmind2  16654  mreiincl  17558  gsumcom2  19950  gsummptnn0fz  19961  gsummoncoe1  22273  mdetralt2  22574  mdetunilem2  22578  ptcldmpt  23579  cnmptcom  23643  elmptrab  23792  isfildlem  23822  dvmptfsum  25942  dvfsumlem2  25994  dvfsumlem4  25996  dvfsumrlim  25998  dvfsum2  26001  coeeq2  26207  dgrle  26208  rlimcnp  26929  lgamgulmlem2  26993  lgseisenlem2  27339  dchrisumlema  27451  dchrisumlem2  27453  dchrisumlem3  27454  nosupbnd1  27678  nosupbnd2  27680  noinfbnd1  27693  noinfbnd2  27695  mpteleeOLD  28964  gropd  29100  grstructd  29101  isch3  31312  atom1d  32424  mo5f  32558  ssiun2sf  32629  iinabrex  32639  ssrelf  32688  fmptcof2  32730  aciunf1lem  32735  nn0min  32894  fsumiunle  32902  esum2dlem  34236  fiunelros  34318  measiun  34362  bnj1385  34974  bnj1468  34988  bnj110  35000  bnj849  35067  bnj900  35071  bnj981  35092  bnj1014  35103  bnj1123  35128  bnj1128  35132  bnj1384  35174  bnj1489  35198  bnj1497  35202  subtr  36496  subtr2  36497  regsfromsetind  36721  currysetlem  37252  currysetlem1  37254  mptsnunlem  37654  finxpreclem2  37706  finxpreclem6  37712  ptrest  37940  poimirlem24  37965  poimirlem25  37966  poimirlem26  37967  poimirlem28  37969  fdc1  38067  ac6s6  38493  fsumshftd  39398  cdleme31sn1  40827  cdleme32fva  40883  cdlemk36  41359  eu6w  43109  fphpd  43244  monotuz  43369  monotoddzz  43371  oddcomabszz  43372  setindtrs  43453  aomclem6  43487  flcidc  43598  rababg  44001  ss2iundf  44086  binomcxplemnotnn0  44783  nfrelp  45376  uzwo4  45484  fiiuncl  45496  disjf1  45613  disjinfi  45622  dmrelrnrel  45655  supxrgere  45763  supxrgelem  45767  supxrge  45768  supxrleubrnmptf  45879  monoordxr  45910  monoord2xr  45912  fsummulc1f  46001  fsumnncl  46002  fsumf1of  46004  fsumiunss  46005  fsumreclf  46006  fsumlessf  46007  fsumsermpt  46009  fmul01  46010  fmuldfeqlem1  46012  fmuldfeq  46013  fmul01lt1lem1  46014  fmul01lt1lem2  46015  fprodexp  46024  fprodabs2  46025  fprodcnlem  46029  climmulf  46034  climexp  46035  climsuse  46038  climrecf  46039  climinff  46041  climaddf  46045  mullimc  46046  idlimc  46056  neglimc  46075  addlimc  46076  0ellimcdiv  46077  limclner  46079  climsubmpt  46088  climreclf  46092  climeldmeqmpt  46096  climfveqmpt  46099  fnlimfvre  46102  climfveqf  46108  climfveqmpt3  46110  climeldmeqf  46111  limsupref  46113  limsupbnd1f  46114  climeqf  46116  climeldmeqmpt3  46117  climinf2  46135  climinf2mpt  46142  climinfmpt  46143  limsupmnf  46149  limsupequz  46151  limsupre2  46153  limsupequzmptf  46159  limsupre3  46161  cncfshift  46302  fprodcncf  46328  dvmptmulf  46365  dvnmptdivc  46366  dvnmul  46371  dvmptfprodlem  46372  dvmptfprod  46373  iblspltprt  46401  stoweidlem3  46431  stoweidlem26  46454  stoweidlem31  46459  stoweidlem34  46462  stoweidlem42  46470  stoweidlem43  46471  stoweidlem48  46476  stoweidlem51  46479  stoweidlem59  46487  fourierdlem86  46620  fourierdlem89  46623  fourierdlem91  46625  fourierdlem112  46646  sge0f1o  46810  sge0lempt  46838  sge0iunmptlemfi  46841  sge0iunmptlemre  46843  sge0fodjrnlem  46844  sge0iunmpt  46846  sge0ltfirpmpt2  46854  sge0isummpt2  46860  sge0xaddlem2  46862  sge0xadd  46863  meadjiun  46894  voliunsge0lem  46900  meaiunincf  46911  meaiuninc3  46913  meaiininc  46915  hoimbl2  47093  vonhoire  47100  vonn0ioo2  47118  vonn0icc2  47120  salpreimagelt  47135  salpreimalegt  47137  salpreimagtge  47153  salpreimaltle  47154  salpreimagtlt  47158  2reu8i  47561  eu2ndop1stv  47573  f1oresf1o2  47739  ichnfimlem  47923  ichreuopeq  47933  reupr  47982  reuopreuprim  47986  2zrngmmgm  48728  nfsetrecs  50161  setrec2fun  50167  pgind  50192