Theorem nfim 1899

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

Syntax hints:   → wi 4  Ⅎwnf 1786

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

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-nf 1787

This theorem is referenced by:  nfor  1907  nfia1  2150  nfnf1  2151  nfnf  2320  nfsbvOLD  2325  cbval2vOLD  2341  sbievg  2361  mof  2563  cbvmow  2603  moexexlem  2628  nfabdwOLD  2931  cbvralfw  3368  cbvralfwOLD  3369  cbvralf  3371  vtocl2gf  3508  vtocl3gf  3509  vtoclgaf  3512  vtocl2gaf  3515  vtocl3gaf  3516  rspct  3547  rspc  3549  ralab2  3634  mob  3652  reu2eqd  3671  reu8nf  3810  csbhypf  3861  cbvralcsf  3877  dfss2f  3911  rspn0OLD  4287  2reu4lem  4456  reusngf  4608  rexreusng  4615  reuprg0  4638  elintab  4890  axrep2  5212  axrep3  5213  reusv2lem4  5324  reusv3  5328  iunopeqop  5435  nfpo  5508  nffr  5563  reuop  6196  frpoinsg  6246  wfisgOLD  6257  fv3  6792  fvmptss  6887  fvmptd3f  6890  fvmptt  6895  fvmptf  6896  fmptco  7001  dff13f  7129  ovmpos  7421  ov2gf  7422  ovmpodf  7429  ov3  7435  tfis  7701  tfinds  7706  tfindes  7709  findes  7749  dfoprab4f  7896  offval22  7928  tfr3  8230  dom2lem  8780  findcard2  8947  findcard2OLD  9056  ac6sfi  9058  frinsg  9509  dfac8clem  9788  aceq1  9873  dfac5lem5  9883  zfcndrep  10370  zfcndinf  10374  pwfseqlem4a  10417  pwfseqlem4  10418  uzind4s  12648  rabssnn0fi  13706  seqof2  13781  rlim2  15205  ello1mpt  15230  o1compt  15296  summolem2a  15427  sumss  15436  fsumclf  15450  fsumsplitf  15454  fsumsplit1  15457  o1fsum  15525  prodmolem2a  15644  fprodn0  15689  fproddivf  15697  fprodsplitf  15698  fprodsplit1f  15700  prmind2  16390  mreiincl  17305  gsumcom2  19576  gsummptnn0fz  19587  gsummoncoe1  21475  mdetralt2  21758  mdetunilem2  21762  ptcldmpt  22765  cnmptcom  22829  elmptrab  22978  isfildlem  23008  dvmptfsum  25139  dvfsumlem2  25191  dvfsumlem4  25193  dvfsumrlim  25195  dvfsum2  25198  coeeq2  25403  dgrle  25404  rlimcnp  26115  lgamgulmlem2  26179  lgseisenlem2  26524  dchrisumlema  26636  dchrisumlem2  26638  dchrisumlem3  26639  mptelee  27263  gropd  27401  grstructd  27402  isch3  29603  atom1d  30715  mo5f  30837  ssiun2sf  30899  iinabrex  30908  ssrelf  30955  fmptcof2  30994  aciunf1lem  30999  nn0min  31134  fsumiunle  31143  esum2dlem  32060  fiunelros  32142  measiun  32186  bnj1385  32812  bnj1468  32826  bnj110  32838  bnj849  32905  bnj900  32909  bnj981  32930  bnj1014  32941  bnj1123  32966  bnj1128  32970  bnj1384  33012  bnj1489  33036  bnj1497  33040  setinds  33754  tfisg  33786  frpoins3xpg  33787  frpoins3xp3g  33788  nosupbnd1  33917  nosupbnd2  33919  noinfbnd1  33932  noinfbnd2  33934  subtr  34503  subtr2  34504  currysetlem  35134  currysetlem1  35136  mptsnunlem  35509  finxpreclem2  35561  finxpreclem6  35567  ptrest  35776  poimirlem24  35801  poimirlem25  35802  poimirlem26  35803  poimirlem28  35805  fdc1  35904  ac6s6  36330  fsumshftd  36966  cdleme31sn1  38395  cdleme32fva  38451  cdlemk36  38927  fphpd  40638  monotuz  40763  monotoddzz  40765  oddcomabszz  40766  setindtrs  40847  aomclem6  40884  flcidc  40999  rababg  41181  ss2iundf  41267  binomcxplemnotnn0  41974  uzwo4  42601  fiiuncl  42613  disjf1  42720  disjinfi  42731  dmrelrnrel  42765  supxrgere  42872  supxrgelem  42876  supxrge  42877  supxrleubrnmptf  42991  monoordxr  43023  monoord2xr  43025  fsummulc1f  43112  fsumnncl  43113  fsumf1of  43115  fsumiunss  43116  fsumreclf  43117  fsumlessf  43118  fsumsermpt  43120  fmul01  43121  fmuldfeqlem1  43123  fmuldfeq  43124  fmul01lt1lem1  43125  fmul01lt1lem2  43126  fprodexp  43135  fprodabs2  43136  fprodcnlem  43140  climmulf  43145  climexp  43146  climsuse  43149  climrecf  43150  climinff  43152  climaddf  43156  mullimc  43157  idlimc  43167  neglimc  43188  addlimc  43189  0ellimcdiv  43190  limclner  43192  climsubmpt  43201  climreclf  43205  climeldmeqmpt  43209  climfveqmpt  43212  fnlimfvre  43215  climfveqf  43221  climfveqmpt3  43223  climeldmeqf  43224  limsupref  43226  limsupbnd1f  43227  climeqf  43229  climeldmeqmpt3  43230  climinf2  43248  climinf2mpt  43255  climinfmpt  43256  limsupmnf  43262  limsupequz  43264  limsupre2  43266  limsupequzmptf  43272  limsupre3  43274  cncfshift  43415  fprodcncf  43441  dvmptmulf  43478  dvnmptdivc  43479  dvnmul  43484  dvmptfprodlem  43485  dvmptfprod  43486  iblspltprt  43514  stoweidlem3  43544  stoweidlem26  43567  stoweidlem31  43572  stoweidlem34  43575  stoweidlem42  43583  stoweidlem43  43584  stoweidlem48  43589  stoweidlem51  43592  stoweidlem59  43600  fourierdlem86  43733  fourierdlem89  43736  fourierdlem91  43738  fourierdlem112  43759  sge0f1o  43920  sge0lempt  43948  sge0iunmptlemfi  43951  sge0iunmptlemre  43953  sge0fodjrnlem  43954  sge0iunmpt  43956  sge0ltfirpmpt2  43964  sge0isummpt2  43970  sge0xaddlem2  43972  sge0xadd  43973  meadjiun  44004  voliunsge0lem  44010  meaiunincf  44021  meaiuninc3  44023  meaiininc  44025  hoimbl2  44203  vonhoire  44210  vonn0ioo2  44228  vonn0icc2  44230  salpreimagelt  44244  salpreimalegt  44246  salpreimagtge  44261  salpreimaltle  44262  salpreimagtlt  44266  2reu8i  44605  eu2ndop1stv  44617  f1oresf1o2  44783  ichnfimlem  44915  ichreuopeq  44925  reupr  44974  reuopreuprim  44978  2zrngmmgm  45504  nfsetrecs  46392  setrec2fun  46398