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  2332  cbvsbvf  2368  mof  2564  cbvmow  2604  moexexlem  2627  cbvralfw  3278  cbvralf  3323  vtocl2gf  3516  vtocl3gf  3517  vtoclgaf  3520  vtocl2gaf  3523  vtocl2gafOLD  3524  vtocl3gaf  3525  vtocl3gafOLD  3526  rspct  3551  rspc  3553  ralab2  3644  mob  3664  reu2eqd  3683  reu8nf  3816  csbhypf  3866  cbvralcsf  3880  dfssf  3913  2reu4lem  4464  reusngf  4619  rexreusng  4624  reuprg0  4647  axrep2  5216  axrep3  5217  reusv2lem4  5339  reusv3  5343  iunopeqop  5470  nfpo  5539  nffr  5598  reuop  6252  frpoinsg  6302  fv3  6853  fvmptss  6955  fvmptd3f  6958  fvmptt  6963  fvmptf  6964  fmptco  7077  dff13f  7204  ovmpos  7509  ov2gf  7510  ovmpodf  7517  ov3  7524  tfisg  7799  tfis  7800  tfinds  7805  tfindes  7808  findes  7845  dfoprab4f  8003  offval22  8032  frpoins3xpg  8084  frpoins3xp3g  8085  tfr3  8332  dom2lem  8933  findcard2  9093  ac6sfi  9188  setinds  9664  frinsg  9669  dfac8clem  9948  aceq1  10033  dfac5lem5  10043  zfcndrep  10531  zfcndinf  10535  pwfseqlem4a  10578  pwfseqlem4  10579  uzind4s  12852  rabssnn0fi  13942  seqof2  14016  rlim2  15452  ello1mpt  15477  o1compt  15543  summolem2a  15671  sumss  15680  fsumclf  15694  fsumsplitf  15698  fsumsplit1  15701  o1fsum  15770  prodmolem2a  15893  fprodn0  15938  fproddivf  15946  fprodsplitf  15947  fprodsplit1f  15949  prmind2  16648  mreiincl  17552  gsumcom2  19944  gsummptnn0fz  19955  gsummoncoe1  22286  mdetralt2  22587  mdetunilem2  22591  ptcldmpt  23592  cnmptcom  23656  elmptrab  23805  isfildlem  23835  dvmptfsum  25955  dvfsumlem2  26007  dvfsumlem4  26009  dvfsumrlim  26011  dvfsum2  26014  coeeq2  26220  dgrle  26221  rlimcnp  26945  lgamgulmlem2  27010  lgseisenlem2  27356  dchrisumlema  27468  dchrisumlem2  27470  dchrisumlem3  27471  nosupbnd1  27695  nosupbnd2  27697  noinfbnd1  27710  noinfbnd2  27712  mpteleeOLD  28981  gropd  29117  grstructd  29118  isch3  31330  atom1d  32442  mo5f  32576  ssiun2sf  32647  iinabrex  32657  ssrelf  32706  fmptcof2  32748  aciunf1lem  32753  nn0min  32912  fsumiunle  32920  esum2dlem  34255  fiunelros  34337  measiun  34381  bnj1385  34993  bnj1468  35007  bnj110  35019  bnj849  35086  bnj900  35090  bnj981  35111  bnj1014  35122  bnj1123  35147  bnj1128  35151  bnj1384  35193  bnj1489  35217  bnj1497  35221  subtr  36515  subtr2  36516  regsfromsetind  36740  currysetlem  37271  currysetlem1  37273  mptsnunlem  37671  finxpreclem2  37723  finxpreclem6  37729  ptrest  37957  poimirlem24  37982  poimirlem25  37983  poimirlem26  37984  poimirlem28  37986  fdc1  38084  ac6s6  38510  fsumshftd  39415  cdleme31sn1  40844  cdleme32fva  40900  cdlemk36  41376  eu6w  43126  fphpd  43265  monotuz  43390  monotoddzz  43392  oddcomabszz  43393  setindtrs  43474  aomclem6  43508  flcidc  43619  rababg  44022  ss2iundf  44107  binomcxplemnotnn0  44804  nfrelp  45397  uzwo4  45505  fiiuncl  45517  disjf1  45634  disjinfi  45643  dmrelrnrel  45676  supxrgere  45784  supxrgelem  45788  supxrge  45789  supxrleubrnmptf  45900  monoordxr  45931  monoord2xr  45933  fsummulc1f  46022  fsumnncl  46023  fsumf1of  46025  fsumiunss  46026  fsumreclf  46027  fsumlessf  46028  fsumsermpt  46030  fmul01  46031  fmuldfeqlem1  46033  fmuldfeq  46034  fmul01lt1lem1  46035  fmul01lt1lem2  46036  fprodexp  46045  fprodabs2  46046  fprodcnlem  46050  climmulf  46055  climexp  46056  climsuse  46059  climrecf  46060  climinff  46062  climaddf  46066  mullimc  46067  idlimc  46077  neglimc  46096  addlimc  46097  0ellimcdiv  46098  limclner  46100  climsubmpt  46109  climreclf  46113  climeldmeqmpt  46117  climfveqmpt  46120  fnlimfvre  46123  climfveqf  46129  climfveqmpt3  46131  climeldmeqf  46132  limsupref  46134  limsupbnd1f  46135  climeqf  46137  climeldmeqmpt3  46138  climinf2  46156  climinf2mpt  46163  climinfmpt  46164  limsupmnf  46170  limsupequz  46172  limsupre2  46174  limsupequzmptf  46180  limsupre3  46182  cncfshift  46323  fprodcncf  46349  dvmptmulf  46386  dvnmptdivc  46387  dvnmul  46392  dvmptfprodlem  46393  dvmptfprod  46394  iblspltprt  46422  stoweidlem3  46452  stoweidlem26  46475  stoweidlem31  46480  stoweidlem34  46483  stoweidlem42  46491  stoweidlem43  46492  stoweidlem48  46497  stoweidlem51  46500  stoweidlem59  46508  fourierdlem86  46641  fourierdlem89  46644  fourierdlem91  46646  fourierdlem112  46667  sge0f1o  46831  sge0lempt  46859  sge0iunmptlemfi  46862  sge0iunmptlemre  46864  sge0fodjrnlem  46865  sge0iunmpt  46867  sge0ltfirpmpt2  46875  sge0isummpt2  46881  sge0xaddlem2  46883  sge0xadd  46884  meadjiun  46915  voliunsge0lem  46921  meaiunincf  46932  meaiuninc3  46934  meaiininc  46936  hoimbl2  47114  vonhoire  47121  vonn0ioo2  47139  vonn0icc2  47141  salpreimagelt  47156  salpreimalegt  47158  salpreimagtge  47174  salpreimaltle  47175  salpreimagtlt  47179  2reu8i  47576  eu2ndop1stv  47588  f1oresf1o2  47754  ichnfimlem  47938  ichreuopeq  47948  reupr  47997  reuopreuprim  48001  2zrngmmgm  48743  nfsetrecs  50176  setrec2fun  50182  pgind  50207