Theorem nfim 1923

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

Syntax hints:   → wi 4  Ⅎwnf 1810

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

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-nf 1811

This theorem is referenced by:  nfor  1931  nfia1  2194  nfnf1  2195  nfnf  2365  cbvsbvf  2401  mof  2597  cbvmow  2637  moexexlem  2660  cbvralfw  3311  cbvralf  3356  vtocl2gf  3545  vtocl3gf  3546  vtoclgaf  3549  vtocl2gaf  3552  vtocl3gaf  3553  rspct  3576  rspc  3578  ralab2  3669  mob  3689  reu2eqd  3708  reu8nf  3839  csbhypf  3889  cbvralcsf  3903  dfssf  3936  2reu4lem  4489  reusngf  4645  rexreusng  4650  reuprg0  4673  axrep2  5245  axrep3  5246  reusv2lem4  5373  reusv3  5377  iunopeqop  5505  iunopeqopOLD  5506  nfpo  5576  nffr  5635  reuop  6295  frpoinsg  6345  fv3  6900  fvmptss  7003  fvmptd3f  7006  fvmptt  7011  fvmptf  7012  fmptco  7126  dff13f  7254  ovmpos  7559  ov2gf  7560  ovmpodf  7567  ov3  7574  tfisg  7849  tfis  7850  tfinds  7855  tfindes  7858  findes  7896  dfoprab4f  8052  offval22  8082  frpoins3xpg  8135  frpoins3xp3g  8136  tfr3  8385  dom2lem  8988  findcard2  9148  ac6sfi  9243  setinds  9717  frinsg  9722  dfac8clem  10015  aceq1  10100  dfac5lem5  10110  zfcndrep  10598  zfcndinf  10602  pwfseqlem4a  10645  pwfseqlem4  10646  uzind4s  12931  rabssnn0fi  14021  seqof2  14095  rlim2  15546  ello1mpt  15571  o1compt  15637  summolem2a  15765  sumss  15774  fsumclf  15788  fsumsplitf  15792  fsumsplit1  15795  o1fsum  15864  prodmolem2a  15987  fprodn0  16032  fproddivf  16040  fprodsplitf  16041  fprodsplit1f  16043  prmind2  16742  mreiincl  17647  gsumcom2  20044  gsummptnn0fz  20055  gsummoncoe1  22436  mdetralt2  22734  mdetunilem2  22738  ptcldmpt  23739  cnmptcom  23803  elmptrab  23952  isfildlem  23982  dvmptfsum  26102  dvfsumlem2  26154  dvfsumlem4  26156  dvfsumrlim  26158  dvfsum2  26161  coeeq2  26367  dgrle  26368  rlimcnp  27095  lgamgulmlem2  27159  lgseisenlem2  27505  dchrisumlema  27617  dchrisumlem2  27619  dchrisumlem3  27620  nosupbnd1  27843  nosupbnd2  27845  noinfbnd1  27858  noinfbnd2  27860  mpteleeOLD  29185  gropd  29321  grstructd  29322  isch3  31533  atom1d  32645  mo5f  32775  ssiun2sf  32844  iinabrex  32854  ssrelf  32900  fmptcof2  32942  aciunf1lem  32947  nn0min  33105  fsumiunle  33113  esum2dlem  34426  fiunelros  34508  measiun  34552  bnj1385  35164  bnj1468  35178  bnj110  35190  bnj849  35257  bnj900  35261  bnj981  35282  bnj1014  35293  bnj1123  35318  bnj1128  35322  bnj1384  35364  bnj1489  35388  bnj1497  35392  subtr  36713  subtr2  36714  regsfromsetind  36938  currysetlem  37468  currysetlem1  37470  mptsnunlem  37871  finxpreclem2  37923  finxpreclem6  37929  ptrest  38157  poimirlem24  38182  poimirlem25  38183  poimirlem26  38184  poimirlem28  38186  fdc1  38284  ac6s6  38710  fsumshftd  39615  cdleme31sn1  41044  cdleme32fva  41100  cdlemk36  41576  eu6w  43299  fphpd  43434  monotuz  43559  monotoddzz  43561  oddcomabszz  43562  setindtrs  43643  aomclem6  43677  flcidc  43788  rababg  44191  ss2iundf  44276  binomcxplemnotnn0  44957  nfrelp  45549  uzwo4  45664  fiiuncl  45676  disjf1  45792  disjinfi  45801  dmrelrnrel  45833  supxrgere  45940  supxrgelem  45944  supxrge  45945  supxrleubrnmptf  46056  monoordxr  46087  monoord2xr  46089  fsummulc1f  46178  fsumnncl  46179  fsumf1of  46181  fsumiunss  46182  fsumreclf  46183  fsumlessf  46184  fsumsermpt  46186  fmul01  46187  fmuldfeqlem1  46189  fmuldfeq  46190  fmul01lt1lem1  46191  fmul01lt1lem2  46192  fprodexp  46201  fprodabs2  46202  fprodcnlem  46206  climmulf  46211  climexp  46212  climsuse  46215  climrecf  46216  climinff  46218  climaddf  46222  mullimc  46223  idlimc  46233  neglimc  46252  addlimc  46253  0ellimcdiv  46254  limclner  46256  climsubmpt  46265  climreclf  46269  climeldmeqmpt  46273  climfveqmpt  46276  fnlimfvre  46279  climfveqf  46285  climfveqmpt3  46287  climeldmeqf  46288  limsupref  46290  limsupbnd1f  46291  climeqf  46293  climeldmeqmpt3  46294  climinf2  46312  climinf2mpt  46319  climinfmpt  46320  limsupmnf  46326  limsupequz  46328  limsupre2  46330  limsupequzmptf  46336  limsupre3  46338  cncfshift  46479  fprodcncf  46505  dvmptmulf  46542  dvnmptdivc  46543  dvnmul  46548  dvmptfprodlem  46549  dvmptfprod  46550  iblspltprt  46578  stoweidlem3  46608  stoweidlem26  46631  stoweidlem31  46636  stoweidlem34  46639  stoweidlem42  46647  stoweidlem43  46648  stoweidlem48  46653  stoweidlem51  46656  stoweidlem59  46664  fourierdlem86  46797  fourierdlem89  46800  fourierdlem91  46802  fourierdlem112  46823  sge0f1o  46987  sge0lempt  47015  sge0iunmptlemfi  47018  sge0iunmptlemre  47020  sge0fodjrnlem  47021  sge0iunmpt  47023  sge0ltfirpmpt2  47031  sge0isummpt2  47037  sge0xaddlem2  47039  sge0xadd  47040  meadjiun  47071  voliunsge0lem  47077  meaiunincf  47088  meaiuninc3  47090  meaiininc  47092  hoimbl2  47270  vonhoire  47277  vonn0ioo2  47295  vonn0icc2  47297  salpreimagelt  47312  salpreimalegt  47314  salpreimagtge  47330  salpreimaltle  47331  salpreimagtlt  47335  2reu8i  47738  eu2ndop1stv  47750  f1oresf1o2  47916  ichnfimlem  48100  ichreuopeq  48110  reupr  48159  reuopreuprim  48163  2zrngmmgm  48905  nfsetrecs  50348  setrec2fun  50354  pgind  50379  nfals  50465  nfrals  50466