Theorem nfim 1926

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

Syntax hints:   → wi 4  Ⅎwnf 1813

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

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-nf 1814

This theorem is referenced by:  nfor  1934  nfia1  2188  nfnf1  2189  nfnf  2359  cbvsbvf  2395  mof  2591  cbvmow  2631  moexexlem  2654  cbvralfw  3305  cbvralf  3349  vtocl2gf  3536  vtocl3gf  3537  vtoclgaf  3540  vtocl2gaf  3543  vtocl3gaf  3544  rspct  3567  rspc  3569  ralab2  3660  mob  3680  reu2eqd  3699  reu8nf  3830  csbhypf  3881  cbvralcsf  3895  dfssf  3928  2reu4lem  4484  reusngf  4640  rexreusng  4645  reuprg0  4668  axrep2  5241  axrep3  5242  reusv2lem4  5372  reusv3  5376  iunopeqop  5504  iunopeqopOLD  5505  nfpo  5575  nffr  5634  reuop  6294  frpoinsg  6344  fv3  6899  fvmptss  7002  fvmptd3f  7005  fvmptt  7010  fvmptf  7011  fmptco  7125  dff13f  7253  ovmpos  7558  ov2gf  7559  ovmpodf  7566  ov3  7573  tfisg  7846  tfis  7847  tfinds  7852  tfindes  7855  findes  7893  dfoprab4f  8049  offval22  8079  frpoins3xpg  8132  frpoins3xp3g  8133  tfr3  8382  dom2lem  8985  findcard2  9145  ac6sfi  9240  setinds  9714  frinsg  9719  dfac8clem  10012  aceq1  10097  dfac5lem5  10107  zfcndrep  10594  zfcndinf  10598  pwfseqlem4a  10641  pwfseqlem4  10642  uzind4s  12927  rabssnn0fi  14018  seqof2  14092  rlim2  15543  ello1mpt  15568  o1compt  15634  summolem2a  15762  sumss  15771  fsumclf  15785  fsumsplitf  15789  fsumsplit1  15792  o1fsum  15861  prodmolem2a  15984  fprodn0  16029  fproddivf  16037  fprodsplitf  16038  fprodsplit1f  16040  prmind2  16738  mreiincl  17643  gsumcom2  20040  gsummptnn0fz  20051  gsummoncoe1  22468  mdetralt2  22766  mdetunilem2  22770  ptcldmpt  23771  cnmptcom  23835  elmptrab  23984  isfildlem  24014  dvmptfsum  26134  dvfsumlem2  26186  dvfsumlem4  26188  dvfsumrlim  26190  dvfsum2  26193  coeeq2  26399  dgrle  26400  rlimcnp  27130  lgamgulmlem2  27194  lgseisenlem2  27540  dchrisumlema  27652  dchrisumlem2  27654  dchrisumlem3  27655  nosupbnd1  27878  nosupbnd2  27880  noinfbnd1  27893  noinfbnd2  27895  mpteleeOLD  29245  gropd  29381  grstructd  29382  isch3  31593  atom1d  32705  mo5f  32835  ssiun2sf  32904  iinabrex  32914  ssrelf  32960  fmptcof2  33002  aciunf1lem  33007  nn0min  33165  fsumiunle  33173  esum2dlem  34482  fiunelros  34564  measiun  34608  bnj1385  35220  bnj1468  35234  bnj110  35246  bnj849  35313  bnj900  35317  bnj981  35338  bnj1014  35349  bnj1123  35374  bnj1128  35378  bnj1384  35420  bnj1489  35444  bnj1497  35448  subtr  36825  subtr2  36826  regsfromsetind  37050  currysetlem  37581  currysetlem1  37583  mptsnunlem  37984  finxpreclem2  38036  finxpreclem6  38042  ptrest  38270  poimirlem24  38295  poimirlem25  38296  poimirlem26  38297  poimirlem28  38299  fdc1  38397  ac6s6  38821  fsumshftd  39726  cdleme31sn1  41155  cdleme32fva  41211  cdlemk36  41687  eu6w  43408  fphpd  43543  monotuz  43668  monotoddzz  43670  oddcomabszz  43671  setindtrs  43752  aomclem6  43786  flcidc  43897  rababg  44300  ss2iundf  44385  binomcxplemnotnn0  45066  nfrelp  45658  uzwo4  45773  fiiuncl  45785  disjf1  45901  disjinfi  45910  dmrelrnrel  45942  supxrgere  46049  supxrgelem  46053  supxrge  46054  supxrleubrnmptf  46165  monoordxr  46196  monoord2xr  46198  fsummulc1f  46287  fsumnncl  46288  fsumf1of  46290  fsumiunss  46291  fsumreclf  46292  fsumlessf  46293  fsumsermpt  46295  fmul01  46296  fmuldfeqlem1  46298  fmuldfeq  46299  fmul01lt1lem1  46300  fmul01lt1lem2  46301  fprodexp  46310  fprodabs2  46311  fprodcnlem  46315  climmulf  46320  climexp  46321  climsuse  46324  climrecf  46325  climinff  46327  climaddf  46331  mullimc  46332  idlimc  46342  neglimc  46361  addlimc  46362  0ellimcdiv  46363  limclner  46365  climsubmpt  46374  climreclf  46378  climeldmeqmpt  46382  climfveqmpt  46385  fnlimfvre  46388  climfveqf  46394  climfveqmpt3  46396  climeldmeqf  46397  limsupref  46399  limsupbnd1f  46400  climeqf  46402  climeldmeqmpt3  46403  climinf2  46421  climinf2mpt  46428  climinfmpt  46429  limsupmnf  46435  limsupequz  46437  limsupre2  46439  limsupequzmptf  46445  limsupre3  46447  cncfshift  46588  fprodcncf  46614  dvmptmulf  46651  dvnmptdivc  46652  dvnmul  46657  dvmptfprodlem  46658  dvmptfprod  46659  iblspltprt  46687  stoweidlem3  46717  stoweidlem26  46740  stoweidlem31  46745  stoweidlem34  46748  stoweidlem42  46756  stoweidlem43  46757  stoweidlem48  46762  stoweidlem51  46765  stoweidlem59  46773  fourierdlem86  46906  fourierdlem89  46909  fourierdlem91  46911  fourierdlem112  46932  sge0f1o  47096  sge0lempt  47124  sge0iunmptlemfi  47127  sge0iunmptlemre  47129  sge0fodjrnlem  47130  sge0iunmpt  47132  sge0ltfirpmpt2  47140  sge0isummpt2  47146  sge0xaddlem2  47148  sge0xadd  47149  meadjiun  47180  voliunsge0lem  47186  meaiunincf  47197  meaiuninc3  47199  meaiininc  47201  hoimbl2  47379  vonhoire  47386  vonn0ioo2  47404  vonn0icc2  47406  salpreimagelt  47421  salpreimalegt  47423  salpreimagtge  47439  salpreimaltle  47440  salpreimagtlt  47444  2reu8i  47850  eu2ndop1stv  47862  f1oresf1o2  48028  ichnfimlem  48212  ichreuopeq  48222  reupr  48271  reuopreuprim  48275  2zrngmmgm  49017  nfsetrecs  50464  setrec2fun  50470  pgind  50495  nfals  50581  nfrals  50582  nfalseu  50612  nfralseu  50613