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 692	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 207  df-an 396  df-ex 1781  df-nf 1785

This theorem is referenced by:  nfor  1905  nfia1  2158  nfnf1  2159  nfnf  2331  cbvsbvf  2367  mof  2563  cbvmow  2603  moexexlem  2626  cbvralfw  3276  cbvralf  3330  vtocl2gf  3527  vtocl3gf  3528  vtoclgaf  3531  vtocl2gaf  3534  vtocl2gafOLD  3535  vtocl3gaf  3536  vtocl3gafOLD  3537  rspct  3562  rspc  3564  ralab2  3655  mob  3675  reu2eqd  3694  reu8nf  3827  csbhypf  3877  cbvralcsf  3891  dfssf  3924  2reu4lem  4476  reusngf  4631  rexreusng  4636  reuprg0  4659  axrep2  5227  axrep3  5228  reusv2lem4  5346  reusv3  5350  iunopeqop  5469  nfpo  5538  nffr  5597  reuop  6251  frpoinsg  6301  fv3  6852  fvmptss  6953  fvmptd3f  6956  fvmptt  6961  fvmptf  6962  fmptco  7074  dff13f  7201  ovmpos  7506  ov2gf  7507  ovmpodf  7514  ov3  7521  tfisg  7796  tfis  7797  tfinds  7802  tfindes  7805  findes  7842  dfoprab4f  8000  offval22  8030  frpoins3xpg  8082  frpoins3xp3g  8083  tfr3  8330  dom2lem  8929  findcard2  9089  ac6sfi  9184  setinds  9658  frinsg  9663  dfac8clem  9942  aceq1  10027  dfac5lem5  10037  zfcndrep  10525  zfcndinf  10529  pwfseqlem4a  10572  pwfseqlem4  10573  uzind4s  12821  rabssnn0fi  13909  seqof2  13983  rlim2  15419  ello1mpt  15444  o1compt  15510  summolem2a  15638  sumss  15647  fsumclf  15661  fsumsplitf  15665  fsumsplit1  15668  o1fsum  15736  prodmolem2a  15857  fprodn0  15902  fproddivf  15910  fprodsplitf  15911  fprodsplit1f  15913  prmind2  16612  mreiincl  17515  gsumcom2  19904  gsummptnn0fz  19915  gsummoncoe1  22252  mdetralt2  22553  mdetunilem2  22557  ptcldmpt  23558  cnmptcom  23622  elmptrab  23771  isfildlem  23801  dvmptfsum  25935  dvfsumlem2  25989  dvfsumlem2OLD  25990  dvfsumlem4  25992  dvfsumrlim  25994  dvfsum2  25997  coeeq2  26203  dgrle  26204  rlimcnp  26931  lgamgulmlem2  26996  lgseisenlem2  27343  dchrisumlema  27455  dchrisumlem2  27457  dchrisumlem3  27458  nosupbnd1  27682  nosupbnd2  27684  noinfbnd1  27697  noinfbnd2  27699  mpteleeOLD  28968  gropd  29104  grstructd  29105  isch3  31316  atom1d  32428  mo5f  32563  ssiun2sf  32634  iinabrex  32644  ssrelf  32693  fmptcof2  32735  aciunf1lem  32740  nn0min  32901  fsumiunle  32910  esum2dlem  34249  fiunelros  34331  measiun  34375  bnj1385  34988  bnj1468  35002  bnj110  35014  bnj849  35081  bnj900  35085  bnj981  35106  bnj1014  35117  bnj1123  35142  bnj1128  35146  bnj1384  35188  bnj1489  35212  bnj1497  35216  subtr  36508  subtr2  36509  regsfromsetind  36669  currysetlem  37146  currysetlem1  37148  mptsnunlem  37543  finxpreclem2  37595  finxpreclem6  37601  ptrest  37820  poimirlem24  37845  poimirlem25  37846  poimirlem26  37847  poimirlem28  37849  fdc1  37947  ac6s6  38373  fsumshftd  39212  cdleme31sn1  40641  cdleme32fva  40697  cdlemk36  41173  eu6w  42919  fphpd  43058  monotuz  43183  monotoddzz  43185  oddcomabszz  43186  setindtrs  43267  aomclem6  43301  flcidc  43412  rababg  43815  ss2iundf  43900  binomcxplemnotnn0  44597  nfrelp  45190  uzwo4  45298  fiiuncl  45310  disjf1  45427  disjinfi  45436  dmrelrnrel  45470  supxrgere  45578  supxrgelem  45582  supxrge  45583  supxrleubrnmptf  45695  monoordxr  45726  monoord2xr  45728  fsummulc1f  45817  fsumnncl  45818  fsumf1of  45820  fsumiunss  45821  fsumreclf  45822  fsumlessf  45823  fsumsermpt  45825  fmul01  45826  fmuldfeqlem1  45828  fmuldfeq  45829  fmul01lt1lem1  45830  fmul01lt1lem2  45831  fprodexp  45840  fprodabs2  45841  fprodcnlem  45845  climmulf  45850  climexp  45851  climsuse  45854  climrecf  45855  climinff  45857  climaddf  45861  mullimc  45862  idlimc  45872  neglimc  45891  addlimc  45892  0ellimcdiv  45893  limclner  45895  climsubmpt  45904  climreclf  45908  climeldmeqmpt  45912  climfveqmpt  45915  fnlimfvre  45918  climfveqf  45924  climfveqmpt3  45926  climeldmeqf  45927  limsupref  45929  limsupbnd1f  45930  climeqf  45932  climeldmeqmpt3  45933  climinf2  45951  climinf2mpt  45958  climinfmpt  45959  limsupmnf  45965  limsupequz  45967  limsupre2  45969  limsupequzmptf  45975  limsupre3  45977  cncfshift  46118  fprodcncf  46144  dvmptmulf  46181  dvnmptdivc  46182  dvnmul  46187  dvmptfprodlem  46188  dvmptfprod  46189  iblspltprt  46217  stoweidlem3  46247  stoweidlem26  46270  stoweidlem31  46275  stoweidlem34  46278  stoweidlem42  46286  stoweidlem43  46287  stoweidlem48  46292  stoweidlem51  46295  stoweidlem59  46303  fourierdlem86  46436  fourierdlem89  46439  fourierdlem91  46441  fourierdlem112  46462  sge0f1o  46626  sge0lempt  46654  sge0iunmptlemfi  46657  sge0iunmptlemre  46659  sge0fodjrnlem  46660  sge0iunmpt  46662  sge0ltfirpmpt2  46670  sge0isummpt2  46676  sge0xaddlem2  46678  sge0xadd  46679  meadjiun  46710  voliunsge0lem  46716  meaiunincf  46727  meaiuninc3  46729  meaiininc  46731  hoimbl2  46909  vonhoire  46916  vonn0ioo2  46934  vonn0icc2  46936  salpreimagelt  46951  salpreimalegt  46953  salpreimagtge  46969  salpreimaltle  46970  salpreimagtlt  46974  2reu8i  47359  eu2ndop1stv  47371  f1oresf1o2  47537  ichnfimlem  47709  ichreuopeq  47719  reupr  47768  reuopreuprim  47772  2zrngmmgm  48498  nfsetrecs  49931  setrec2fun  49937  pgind  49962