Theorem nfim 1929

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

This proof depends on syntax axioms:   → wi 4  Ⅎwnf 1816

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-nf 1817

This theorem is used by:  nfor  1937  nfia1  2191  nfnf1  2192  nfnf  2361  cbvsbvf  2397  mof  2593  cbvmow  2633  moexexlem  2656  cbvralfw  3307  cbvralf  3351  vtocl2gf  3538  vtocl3gf  3539  vtoclgaf  3542  vtocl2gaf  3545  vtocl3gaf  3546  rspct  3569  rspc  3571  ralab2  3662  mob  3682  reu2eqd  3701  reu8nf  3831  csbhypf  3882  cbvralcsf  3896  dfssf  3929  2reu4lem  4486  reusngf  4642  rexreusng  4647  reuprg0  4670  axrep2  5243  axrep3  5244  reusv2lem4  5374  reusv3  5378  iunopeqop  5506  iunopeqopOLD  5507  nfpo  5577  nffr  5636  reuop  6298  frpoinsg  6348  fv3  6903  fvmptss  7006  fvmptd3f  7009  fvmptt  7014  fvmptf  7015  fmptco  7129  dff13f  7258  ovmpos  7567  ov2gf  7568  ovmpodf  7575  ov3  7582  tfisg  7856  tfis  7857  tfinds  7862  tfindes  7865  findes  7903  dfoprab4f  8059  offval22  8089  frpoins3xpg  8142  frpoins3xp3g  8143  tfr3  8392  dom2lem  8995  findcard2  9156  ac6sfi  9251  setinds  9725  frinsg  9730  dfac8clem  10032  aceq1  10117  dfac5lem5  10127  zfcndrep  10614  zfcndinf  10618  pwfseqlem4a  10661  pwfseqlem4  10662  uzind4s  12948  rabssnn0fi  14040  seqof2  14114  rlim2  15571  ello1mpt  15596  o1compt  15662  summolem2a  15789  sumss  15798  fsumclf  15812  fsumsplitf  15816  fsumsplit1  15819  o1fsum  15888  prodmolem2a  16011  fprodn0  16056  fproddivf  16064  fprodsplitf  16065  fprodsplit1f  16067  prmind2  16765  mreiincl  17670  gsumcom2  20089  gsummptnn0fz  20100  gsummoncoe1  22518  mdetralt2  22816  mdetunilem2  22820  ptcldmpt  23822  cnmptcom  23886  elmptrab  24035  isfildlem  24065  dvmptfsum  26185  dvfsumlem2  26237  dvfsumlem4  26239  dvfsumrlim  26241  dvfsum2  26244  coeeq2  26450  dgrle  26451  rlimcnp  27181  lgamgulmlem2  27245  lgseisenlem2  27591  dchrisumlema  27703  dchrisumlem2  27705  dchrisumlem3  27706  nosupbnd1  27929  nosupbnd2  27931  noinfbnd1  27944  noinfbnd2  27946  mpteleeOLD  29300  gropd  29436  grstructd  29437  isch3  31664  atom1d  32776  mo5f  32906  ssiun2sf  32975  iinabrex  32985  ssrelf  33031  fmptcof2  33073  aciunf1lem  33078  nn0min  33235  fsumiunle  33243  esum2dlem  34546  fiunelros  34629  measiun  34673  bnj1385  35285  bnj1468  35299  bnj110  35311  bnj849  35378  bnj900  35382  bnj981  35403  bnj1014  35414  bnj1123  35439  bnj1128  35443  bnj1384  35485  bnj1489  35509  bnj1497  35513  subtr  36882  subtr2  36883  regsfromsetind  37107  currysetlem  37638  currysetlem1  37640  mptsnunlem  38041  finxpreclem2  38093  finxpreclem6  38099  ptrest  38327  poimirlem24  38352  poimirlem25  38353  poimirlem26  38354  poimirlem28  38356  fdc1  38455  ac6s6  38879  fsumshftd  39784  cdleme31sn1  41213  cdleme32fva  41269  cdlemk36  41745  eu6w  43466  fphpd  43601  monotuz  43726  monotoddzz  43728  oddcomabszz  43729  setindtrs  43810  aomclem6  43844  flcidc  43955  rababg  44358  ss2iundf  44443  binomcxplemnotnn0  45124  nfrelp  45716  uzwo4  45831  fiiuncl  45843  disjf1  45959  disjinfi  45968  dmrelrnrel  46000  supxrgere  46107  supxrgelem  46111  supxrge  46112  supxrleubrnmptf  46223  monoordxr  46254  monoord2xr  46256  fsummulc1f  46345  fsumnncl  46346  fsumf1of  46348  fsumiunss  46349  fsumreclf  46350  fsumlessf  46351  fsumsermpt  46353  fmul01  46354  fmuldfeqlem1  46356  fmuldfeq  46357  fmul01lt1lem1  46358  fmul01lt1lem2  46359  fprodexp  46368  fprodabs2  46369  fprodcnlem  46373  climmulf  46378  climexp  46379  climsuse  46382  climrecf  46383  climinff  46385  climaddf  46389  mullimc  46390  idlimc  46400  neglimc  46419  addlimc  46420  0ellimcdiv  46421  limclner  46423  climsubmpt  46432  climreclf  46436  climeldmeqmpt  46440  climfveqmpt  46443  fnlimfvre  46446  climfveqf  46452  climfveqmpt3  46454  climeldmeqf  46455  limsupref  46457  limsupbnd1f  46458  climeqf  46460  climeldmeqmpt3  46461  climinf2  46479  climinf2mpt  46486  climinfmpt  46487  limsupmnf  46493  limsupequz  46495  limsupre2  46497  limsupequzmptf  46503  limsupre3  46505  cncfshift  46646  fprodcncf  46672  dvmptmulf  46709  dvnmptdivc  46710  dvnmul  46715  dvmptfprodlem  46716  dvmptfprod  46717  iblspltprt  46745  stoweidlem3  46775  stoweidlem26  46798  stoweidlem31  46803  stoweidlem34  46806  stoweidlem42  46814  stoweidlem43  46815  stoweidlem48  46820  stoweidlem51  46823  stoweidlem59  46831  fourierdlem86  46964  fourierdlem89  46967  fourierdlem91  46969  fourierdlem112  46990  sge0f1o  47154  sge0lempt  47182  sge0iunmptlemfi  47185  sge0iunmptlemre  47187  sge0fodjrnlem  47188  sge0iunmpt  47190  sge0ltfirpmpt2  47198  sge0isummpt2  47204  sge0xaddlem2  47206  sge0xadd  47207  meadjiun  47238  voliunsge0lem  47244  meaiunincf  47255  meaiuninc3  47257  meaiininc  47259  hoimbl2  47437  vonhoire  47444  vonn0ioo2  47462  vonn0icc2  47464  salpreimagelt  47479  salpreimalegt  47481  salpreimagtge  47497  salpreimaltle  47498  salpreimagtlt  47502  2reu8i  47908  eu2ndop1stv  47920  f1oresf1o2  48086  ichnfimlem  48270  ichreuopeq  48280  reupr  48329  reuopreuprim  48333  2zrngmmgm  49074  nfsetrecs  50521  setrec2fun  50527  pgind  50552  nfals  50638  nfrals  50639  nfalseu  50669  nfralseu  50670