Theorem nfim 1897

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

Syntax hints:   → wi 4  Ⅎwnf 1784

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

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-nf 1785

This theorem is referenced by:  nfor  1905  nfia1  2158  nfnf1  2159  nfnf  2329  cbvsbvf  2365  mof  2561  cbvmow  2601  moexexlem  2624  cbvralfw  3274  cbvralf  3328  vtocl2gf  3525  vtocl3gf  3526  vtoclgaf  3529  vtocl2gaf  3532  vtocl2gafOLD  3533  vtocl3gaf  3534  vtocl3gafOLD  3535  rspct  3560  rspc  3562  ralab2  3653  mob  3673  reu2eqd  3692  reu8nf  3825  csbhypf  3875  cbvralcsf  3889  dfssf  3922  2reu4lem  4474  reusngf  4629  rexreusng  4634  reuprg0  4657  axrep2  5225  axrep3  5226  reusv2lem4  5344  reusv3  5348  iunopeqop  5467  nfpo  5536  nffr  5595  reuop  6249  frpoinsg  6299  fv3  6850  fvmptss  6951  fvmptd3f  6954  fvmptt  6959  fvmptf  6960  fmptco  7072  dff13f  7199  ovmpos  7504  ov2gf  7505  ovmpodf  7512  ov3  7519  tfisg  7794  tfis  7795  tfinds  7800  tfindes  7803  findes  7840  dfoprab4f  7998  offval22  8028  frpoins3xpg  8080  frpoins3xp3g  8081  tfr3  8328  dom2lem  8927  findcard2  9087  ac6sfi  9182  setinds  9656  frinsg  9661  dfac8clem  9940  aceq1  10025  dfac5lem5  10035  zfcndrep  10523  zfcndinf  10527  pwfseqlem4a  10570  pwfseqlem4  10571  uzind4s  12819  rabssnn0fi  13907  seqof2  13981  rlim2  15417  ello1mpt  15442  o1compt  15508  summolem2a  15636  sumss  15645  fsumclf  15659  fsumsplitf  15663  fsumsplit1  15666  o1fsum  15734  prodmolem2a  15855  fprodn0  15900  fproddivf  15908  fprodsplitf  15909  fprodsplit1f  15911  prmind2  16610  mreiincl  17513  gsumcom2  19902  gsummptnn0fz  19913  gsummoncoe1  22250  mdetralt2  22551  mdetunilem2  22555  ptcldmpt  23556  cnmptcom  23620  elmptrab  23769  isfildlem  23799  dvmptfsum  25933  dvfsumlem2  25987  dvfsumlem2OLD  25988  dvfsumlem4  25990  dvfsumrlim  25992  dvfsum2  25995  coeeq2  26201  dgrle  26202  rlimcnp  26929  lgamgulmlem2  26994  lgseisenlem2  27341  dchrisumlema  27453  dchrisumlem2  27455  dchrisumlem3  27456  nosupbnd1  27680  nosupbnd2  27682  noinfbnd1  27695  noinfbnd2  27697  mpteleeOLD  28917  gropd  29053  grstructd  29054  isch3  31265  atom1d  32377  mo5f  32512  ssiun2sf  32583  iinabrex  32593  ssrelf  32642  fmptcof2  32684  aciunf1lem  32689  nn0min  32850  fsumiunle  32859  esum2dlem  34198  fiunelros  34280  measiun  34324  bnj1385  34937  bnj1468  34951  bnj110  34963  bnj849  35030  bnj900  35034  bnj981  35055  bnj1014  35066  bnj1123  35091  bnj1128  35095  bnj1384  35137  bnj1489  35161  bnj1497  35165  subtr  36457  subtr2  36458  currysetlem  37089  currysetlem1  37091  mptsnunlem  37482  finxpreclem2  37534  finxpreclem6  37540  ptrest  37759  poimirlem24  37784  poimirlem25  37785  poimirlem26  37786  poimirlem28  37788  fdc1  37886  ac6s6  38312  fsumshftd  39151  cdleme31sn1  40580  cdleme32fva  40636  cdlemk36  41112  eu6w  42861  fphpd  43000  monotuz  43125  monotoddzz  43127  oddcomabszz  43128  setindtrs  43209  aomclem6  43243  flcidc  43354  rababg  43757  ss2iundf  43842  binomcxplemnotnn0  44539  nfrelp  45132  uzwo4  45240  fiiuncl  45252  disjf1  45369  disjinfi  45378  dmrelrnrel  45412  supxrgere  45520  supxrgelem  45524  supxrge  45525  supxrleubrnmptf  45637  monoordxr  45668  monoord2xr  45670  fsummulc1f  45759  fsumnncl  45760  fsumf1of  45762  fsumiunss  45763  fsumreclf  45764  fsumlessf  45765  fsumsermpt  45767  fmul01  45768  fmuldfeqlem1  45770  fmuldfeq  45771  fmul01lt1lem1  45772  fmul01lt1lem2  45773  fprodexp  45782  fprodabs2  45783  fprodcnlem  45787  climmulf  45792  climexp  45793  climsuse  45796  climrecf  45797  climinff  45799  climaddf  45803  mullimc  45804  idlimc  45814  neglimc  45833  addlimc  45834  0ellimcdiv  45835  limclner  45837  climsubmpt  45846  climreclf  45850  climeldmeqmpt  45854  climfveqmpt  45857  fnlimfvre  45860  climfveqf  45866  climfveqmpt3  45868  climeldmeqf  45869  limsupref  45871  limsupbnd1f  45872  climeqf  45874  climeldmeqmpt3  45875  climinf2  45893  climinf2mpt  45900  climinfmpt  45901  limsupmnf  45907  limsupequz  45909  limsupre2  45911  limsupequzmptf  45917  limsupre3  45919  cncfshift  46060  fprodcncf  46086  dvmptmulf  46123  dvnmptdivc  46124  dvnmul  46129  dvmptfprodlem  46130  dvmptfprod  46131  iblspltprt  46159  stoweidlem3  46189  stoweidlem26  46212  stoweidlem31  46217  stoweidlem34  46220  stoweidlem42  46228  stoweidlem43  46229  stoweidlem48  46234  stoweidlem51  46237  stoweidlem59  46245  fourierdlem86  46378  fourierdlem89  46381  fourierdlem91  46383  fourierdlem112  46404  sge0f1o  46568  sge0lempt  46596  sge0iunmptlemfi  46599  sge0iunmptlemre  46601  sge0fodjrnlem  46602  sge0iunmpt  46604  sge0ltfirpmpt2  46612  sge0isummpt2  46618  sge0xaddlem2  46620  sge0xadd  46621  meadjiun  46652  voliunsge0lem  46658  meaiunincf  46669  meaiuninc3  46671  meaiininc  46673  hoimbl2  46851  vonhoire  46858  vonn0ioo2  46876  vonn0icc2  46878  salpreimagelt  46893  salpreimalegt  46895  salpreimagtge  46911  salpreimaltle  46912  salpreimagtlt  46916  2reu8i  47301  eu2ndop1stv  47313  f1oresf1o2  47479  ichnfimlem  47651  ichreuopeq  47661  reupr  47710  reuopreuprim  47714  2zrngmmgm  48440  nfsetrecs  49873  setrec2fun  49879  pgind  49904