Theorem nfim 1896

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

Syntax hints:   → wi 4  Ⅎwnf 1783

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

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-nf 1784

This theorem is referenced by:  nfor  1904  nfia1  2153  nfnf1  2154  nfnf  2326  nfsbvOLD  2331  cbvsbvf  2366  mof  2563  cbvmow  2603  moexexlem  2626  cbvralfw  3304  cbvralf  3360  vtocl2gf  3572  vtocl3gf  3573  vtoclgaf  3576  vtocl2gaf  3579  vtocl2gafOLD  3580  vtocl3gaf  3581  vtocl3gafOLD  3582  rspct  3608  rspc  3610  ralab2  3703  mob  3723  reu2eqd  3742  reu8nf  3877  csbhypf  3927  cbvralcsf  3941  dfssf  3974  2reu4lem  4522  reusngf  4674  rexreusng  4679  reuprg0  4702  elintabOLD  4959  axrep2  5282  axrep3  5283  reusv2lem4  5401  reusv3  5405  iunopeqop  5526  nfpo  5598  nffr  5658  reuop  6313  frpoinsg  6364  wfisgOLD  6375  fv3  6924  fvmptss  7028  fvmptd3f  7031  fvmptt  7036  fvmptf  7037  fmptco  7149  dff13f  7276  ovmpos  7581  ov2gf  7582  ovmpodf  7589  ov3  7596  tfisg  7875  tfis  7876  tfinds  7881  tfindes  7884  findes  7922  dfoprab4f  8081  offval22  8113  frpoins3xpg  8165  frpoins3xp3g  8166  tfr3  8439  dom2lem  9032  findcard2  9204  ac6sfi  9320  frinsg  9791  dfac8clem  10072  aceq1  10157  dfac5lem5  10167  zfcndrep  10654  zfcndinf  10658  pwfseqlem4a  10701  pwfseqlem4  10702  uzind4s  12950  rabssnn0fi  14027  seqof2  14101  rlim2  15532  ello1mpt  15557  o1compt  15623  summolem2a  15751  sumss  15760  fsumclf  15774  fsumsplitf  15778  fsumsplit1  15781  o1fsum  15849  prodmolem2a  15970  fprodn0  16015  fproddivf  16023  fprodsplitf  16024  fprodsplit1f  16026  prmind2  16722  mreiincl  17639  gsumcom2  19993  gsummptnn0fz  20004  gsummoncoe1  22312  mdetralt2  22615  mdetunilem2  22619  ptcldmpt  23622  cnmptcom  23686  elmptrab  23835  isfildlem  23865  dvmptfsum  26013  dvfsumlem2  26067  dvfsumlem2OLD  26068  dvfsumlem4  26070  dvfsumrlim  26072  dvfsum2  26075  coeeq2  26281  dgrle  26282  rlimcnp  27008  lgamgulmlem2  27073  lgseisenlem2  27420  dchrisumlema  27532  dchrisumlem2  27534  dchrisumlem3  27535  nosupbnd1  27759  nosupbnd2  27761  noinfbnd1  27774  noinfbnd2  27776  mptelee  28910  gropd  29048  grstructd  29049  isch3  31260  atom1d  32372  mo5f  32508  ssiun2sf  32572  iinabrex  32582  ssrelf  32627  fmptcof2  32667  aciunf1lem  32672  nn0min  32822  fsumiunle  32831  esum2dlem  34093  fiunelros  34175  measiun  34219  bnj1385  34846  bnj1468  34860  bnj110  34872  bnj849  34939  bnj900  34943  bnj981  34964  bnj1014  34975  bnj1123  35000  bnj1128  35004  bnj1384  35046  bnj1489  35070  bnj1497  35074  setinds  35779  subtr  36315  subtr2  36316  currysetlem  36946  currysetlem1  36948  mptsnunlem  37339  finxpreclem2  37391  finxpreclem6  37397  ptrest  37626  poimirlem24  37651  poimirlem25  37652  poimirlem26  37653  poimirlem28  37655  fdc1  37753  ac6s6  38179  fsumshftd  38953  cdleme31sn1  40383  cdleme32fva  40439  cdlemk36  40915  eu6w  42686  fphpd  42827  monotuz  42953  monotoddzz  42955  oddcomabszz  42956  setindtrs  43037  aomclem6  43071  flcidc  43182  rababg  43587  ss2iundf  43672  binomcxplemnotnn0  44375  nfrelp  44970  uzwo4  45058  fiiuncl  45070  disjf1  45188  disjinfi  45197  dmrelrnrel  45231  supxrgere  45344  supxrgelem  45348  supxrge  45349  supxrleubrnmptf  45462  monoordxr  45493  monoord2xr  45495  fsummulc1f  45586  fsumnncl  45587  fsumf1of  45589  fsumiunss  45590  fsumreclf  45591  fsumlessf  45592  fsumsermpt  45594  fmul01  45595  fmuldfeqlem1  45597  fmuldfeq  45598  fmul01lt1lem1  45599  fmul01lt1lem2  45600  fprodexp  45609  fprodabs2  45610  fprodcnlem  45614  climmulf  45619  climexp  45620  climsuse  45623  climrecf  45624  climinff  45626  climaddf  45630  mullimc  45631  idlimc  45641  neglimc  45662  addlimc  45663  0ellimcdiv  45664  limclner  45666  climsubmpt  45675  climreclf  45679  climeldmeqmpt  45683  climfveqmpt  45686  fnlimfvre  45689  climfveqf  45695  climfveqmpt3  45697  climeldmeqf  45698  limsupref  45700  limsupbnd1f  45701  climeqf  45703  climeldmeqmpt3  45704  climinf2  45722  climinf2mpt  45729  climinfmpt  45730  limsupmnf  45736  limsupequz  45738  limsupre2  45740  limsupequzmptf  45746  limsupre3  45748  cncfshift  45889  fprodcncf  45915  dvmptmulf  45952  dvnmptdivc  45953  dvnmul  45958  dvmptfprodlem  45959  dvmptfprod  45960  iblspltprt  45988  stoweidlem3  46018  stoweidlem26  46041  stoweidlem31  46046  stoweidlem34  46049  stoweidlem42  46057  stoweidlem43  46058  stoweidlem48  46063  stoweidlem51  46066  stoweidlem59  46074  fourierdlem86  46207  fourierdlem89  46210  fourierdlem91  46212  fourierdlem112  46233  sge0f1o  46397  sge0lempt  46425  sge0iunmptlemfi  46428  sge0iunmptlemre  46430  sge0fodjrnlem  46431  sge0iunmpt  46433  sge0ltfirpmpt2  46441  sge0isummpt2  46447  sge0xaddlem2  46449  sge0xadd  46450  meadjiun  46481  voliunsge0lem  46487  meaiunincf  46498  meaiuninc3  46500  meaiininc  46502  hoimbl2  46680  vonhoire  46687  vonn0ioo2  46705  vonn0icc2  46707  salpreimagelt  46722  salpreimalegt  46724  salpreimagtge  46740  salpreimaltle  46741  salpreimagtlt  46745  2reu8i  47125  eu2ndop1stv  47137  f1oresf1o2  47303  ichnfimlem  47450  ichreuopeq  47460  reupr  47509  reuopreuprim  47513  2zrngmmgm  48168  nfsetrecs  49205  setrec2fun  49211  pgind  49236