Theorem nfim 1896

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

Syntax hints:   → wi 4  Ⅎwnf 1783

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

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-nf 1784

This theorem is referenced by:  nfor  1904  nfia1  2154  nfnf1  2155  nfnf  2325  cbvsbvf  2361  mof  2556  cbvmow  2596  moexexlem  2619  cbvralfw  3278  cbvralf  3334  vtocl2gf  3538  vtocl3gf  3539  vtoclgaf  3542  vtocl2gaf  3545  vtocl2gafOLD  3546  vtocl3gaf  3547  vtocl3gafOLD  3548  rspct  3574  rspc  3576  ralab2  3668  mob  3688  reu2eqd  3707  reu8nf  3840  csbhypf  3890  cbvralcsf  3904  dfssf  3937  2reu4lem  4485  reusngf  4638  rexreusng  4643  reuprg0  4666  elintabOLD  4923  axrep2  5237  axrep3  5238  reusv2lem4  5356  reusv3  5360  iunopeqop  5481  nfpo  5552  nffr  5611  reuop  6266  frpoinsg  6316  fv3  6876  fvmptss  6980  fvmptd3f  6983  fvmptt  6988  fvmptf  6989  fmptco  7101  dff13f  7230  ovmpos  7537  ov2gf  7538  ovmpodf  7545  ov3  7552  tfisg  7830  tfis  7831  tfinds  7836  tfindes  7839  findes  7876  dfoprab4f  8035  offval22  8067  frpoins3xpg  8119  frpoins3xp3g  8120  tfr3  8367  dom2lem  8963  findcard2  9128  ac6sfi  9231  frinsg  9704  dfac8clem  9985  aceq1  10070  dfac5lem5  10080  zfcndrep  10567  zfcndinf  10571  pwfseqlem4a  10614  pwfseqlem4  10615  uzind4s  12867  rabssnn0fi  13951  seqof2  14025  rlim2  15462  ello1mpt  15487  o1compt  15553  summolem2a  15681  sumss  15690  fsumclf  15704  fsumsplitf  15708  fsumsplit1  15711  o1fsum  15779  prodmolem2a  15900  fprodn0  15945  fproddivf  15953  fprodsplitf  15954  fprodsplit1f  15956  prmind2  16655  mreiincl  17557  gsumcom2  19905  gsummptnn0fz  19916  gsummoncoe1  22195  mdetralt2  22496  mdetunilem2  22500  ptcldmpt  23501  cnmptcom  23565  elmptrab  23714  isfildlem  23744  dvmptfsum  25879  dvfsumlem2  25933  dvfsumlem2OLD  25934  dvfsumlem4  25936  dvfsumrlim  25938  dvfsum2  25941  coeeq2  26147  dgrle  26148  rlimcnp  26875  lgamgulmlem2  26940  lgseisenlem2  27287  dchrisumlema  27399  dchrisumlem2  27401  dchrisumlem3  27402  nosupbnd1  27626  nosupbnd2  27628  noinfbnd1  27641  noinfbnd2  27643  mptelee  28822  gropd  28958  grstructd  28959  isch3  31170  atom1d  32282  mo5f  32418  ssiun2sf  32488  iinabrex  32498  ssrelf  32543  fmptcof2  32581  aciunf1lem  32586  nn0min  32745  fsumiunle  32754  esum2dlem  34082  fiunelros  34164  measiun  34208  bnj1385  34822  bnj1468  34836  bnj110  34848  bnj849  34915  bnj900  34919  bnj981  34940  bnj1014  34951  bnj1123  34976  bnj1128  34980  bnj1384  35022  bnj1489  35046  bnj1497  35050  setinds  35766  subtr  36302  subtr2  36303  currysetlem  36933  currysetlem1  36935  mptsnunlem  37326  finxpreclem2  37378  finxpreclem6  37384  ptrest  37613  poimirlem24  37638  poimirlem25  37639  poimirlem26  37640  poimirlem28  37642  fdc1  37740  ac6s6  38166  fsumshftd  38945  cdleme31sn1  40375  cdleme32fva  40431  cdlemk36  40907  eu6w  42664  fphpd  42804  monotuz  42930  monotoddzz  42932  oddcomabszz  42933  setindtrs  43014  aomclem6  43048  flcidc  43159  rababg  43563  ss2iundf  43648  binomcxplemnotnn0  44345  nfrelp  44939  uzwo4  45047  fiiuncl  45059  disjf1  45177  disjinfi  45186  dmrelrnrel  45220  supxrgere  45329  supxrgelem  45333  supxrge  45334  supxrleubrnmptf  45447  monoordxr  45478  monoord2xr  45480  fsummulc1f  45569  fsumnncl  45570  fsumf1of  45572  fsumiunss  45573  fsumreclf  45574  fsumlessf  45575  fsumsermpt  45577  fmul01  45578  fmuldfeqlem1  45580  fmuldfeq  45581  fmul01lt1lem1  45582  fmul01lt1lem2  45583  fprodexp  45592  fprodabs2  45593  fprodcnlem  45597  climmulf  45602  climexp  45603  climsuse  45606  climrecf  45607  climinff  45609  climaddf  45613  mullimc  45614  idlimc  45624  neglimc  45645  addlimc  45646  0ellimcdiv  45647  limclner  45649  climsubmpt  45658  climreclf  45662  climeldmeqmpt  45666  climfveqmpt  45669  fnlimfvre  45672  climfveqf  45678  climfveqmpt3  45680  climeldmeqf  45681  limsupref  45683  limsupbnd1f  45684  climeqf  45686  climeldmeqmpt3  45687  climinf2  45705  climinf2mpt  45712  climinfmpt  45713  limsupmnf  45719  limsupequz  45721  limsupre2  45723  limsupequzmptf  45729  limsupre3  45731  cncfshift  45872  fprodcncf  45898  dvmptmulf  45935  dvnmptdivc  45936  dvnmul  45941  dvmptfprodlem  45942  dvmptfprod  45943  iblspltprt  45971  stoweidlem3  46001  stoweidlem26  46024  stoweidlem31  46029  stoweidlem34  46032  stoweidlem42  46040  stoweidlem43  46041  stoweidlem48  46046  stoweidlem51  46049  stoweidlem59  46057  fourierdlem86  46190  fourierdlem89  46193  fourierdlem91  46195  fourierdlem112  46216  sge0f1o  46380  sge0lempt  46408  sge0iunmptlemfi  46411  sge0iunmptlemre  46413  sge0fodjrnlem  46414  sge0iunmpt  46416  sge0ltfirpmpt2  46424  sge0isummpt2  46430  sge0xaddlem2  46432  sge0xadd  46433  meadjiun  46464  voliunsge0lem  46470  meaiunincf  46481  meaiuninc3  46483  meaiininc  46485  hoimbl2  46663  vonhoire  46670  vonn0ioo2  46688  vonn0icc2  46690  salpreimagelt  46705  salpreimalegt  46707  salpreimagtge  46723  salpreimaltle  46724  salpreimagtlt  46728  2reu8i  47114  eu2ndop1stv  47126  f1oresf1o2  47292  ichnfimlem  47464  ichreuopeq  47474  reupr  47523  reuopreuprim  47527  2zrngmmgm  48240  nfsetrecs  49675  setrec2fun  49681  pgind  49706