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  2154  nfnf1  2155  nfnf  2325  cbvsbvf  2361  mof  2556  cbvmow  2596  moexexlem  2619  cbvralfw  3269  cbvralf  3323  vtocl2gf  3527  vtocl3gf  3528  vtoclgaf  3531  vtocl2gaf  3534  vtocl2gafOLD  3535  vtocl3gaf  3536  vtocl3gafOLD  3537  rspct  3563  rspc  3565  ralab2  3657  mob  3677  reu2eqd  3696  reu8nf  3829  csbhypf  3879  cbvralcsf  3893  dfssf  3926  2reu4lem  4473  reusngf  4626  rexreusng  4631  reuprg0  4654  elintabOLD  4909  axrep2  5221  axrep3  5222  reusv2lem4  5340  reusv3  5344  iunopeqop  5464  nfpo  5533  nffr  5592  reuop  6241  frpoinsg  6291  fv3  6840  fvmptss  6942  fvmptd3f  6945  fvmptt  6950  fvmptf  6951  fmptco  7063  dff13f  7192  ovmpos  7497  ov2gf  7498  ovmpodf  7505  ov3  7512  tfisg  7787  tfis  7788  tfinds  7793  tfindes  7796  findes  7833  dfoprab4f  7991  offval22  8021  frpoins3xpg  8073  frpoins3xp3g  8074  tfr3  8321  dom2lem  8917  findcard2  9078  ac6sfi  9173  frinsg  9647  dfac8clem  9926  aceq1  10011  dfac5lem5  10021  zfcndrep  10508  zfcndinf  10512  pwfseqlem4a  10555  pwfseqlem4  10556  uzind4s  12809  rabssnn0fi  13893  seqof2  13967  rlim2  15403  ello1mpt  15428  o1compt  15494  summolem2a  15622  sumss  15631  fsumclf  15645  fsumsplitf  15649  fsumsplit1  15652  o1fsum  15720  prodmolem2a  15841  fprodn0  15886  fproddivf  15894  fprodsplitf  15895  fprodsplit1f  15897  prmind2  16596  mreiincl  17498  gsumcom2  19854  gsummptnn0fz  19865  gsummoncoe1  22193  mdetralt2  22494  mdetunilem2  22498  ptcldmpt  23499  cnmptcom  23563  elmptrab  23712  isfildlem  23742  dvmptfsum  25877  dvfsumlem2  25931  dvfsumlem2OLD  25932  dvfsumlem4  25934  dvfsumrlim  25936  dvfsum2  25939  coeeq2  26145  dgrle  26146  rlimcnp  26873  lgamgulmlem2  26938  lgseisenlem2  27285  dchrisumlema  27397  dchrisumlem2  27399  dchrisumlem3  27400  nosupbnd1  27624  nosupbnd2  27626  noinfbnd1  27639  noinfbnd2  27641  mptelee  28840  gropd  28976  grstructd  28977  isch3  31185  atom1d  32297  mo5f  32433  ssiun2sf  32503  iinabrex  32513  ssrelf  32560  fmptcof2  32600  aciunf1lem  32605  nn0min  32765  fsumiunle  32774  esum2dlem  34059  fiunelros  34141  measiun  34185  bnj1385  34799  bnj1468  34813  bnj110  34825  bnj849  34892  bnj900  34896  bnj981  34917  bnj1014  34928  bnj1123  34953  bnj1128  34957  bnj1384  34999  bnj1489  35023  bnj1497  35027  setinds  35752  subtr  36288  subtr2  36289  currysetlem  36919  currysetlem1  36921  mptsnunlem  37312  finxpreclem2  37364  finxpreclem6  37370  ptrest  37599  poimirlem24  37624  poimirlem25  37625  poimirlem26  37626  poimirlem28  37628  fdc1  37726  ac6s6  38152  fsumshftd  38931  cdleme31sn1  40360  cdleme32fva  40416  cdlemk36  40892  eu6w  42649  fphpd  42789  monotuz  42914  monotoddzz  42916  oddcomabszz  42917  setindtrs  42998  aomclem6  43032  flcidc  43143  rababg  43547  ss2iundf  43632  binomcxplemnotnn0  44329  nfrelp  44923  uzwo4  45031  fiiuncl  45043  disjf1  45161  disjinfi  45170  dmrelrnrel  45204  supxrgere  45313  supxrgelem  45317  supxrge  45318  supxrleubrnmptf  45430  monoordxr  45461  monoord2xr  45463  fsummulc1f  45552  fsumnncl  45553  fsumf1of  45555  fsumiunss  45556  fsumreclf  45557  fsumlessf  45558  fsumsermpt  45560  fmul01  45561  fmuldfeqlem1  45563  fmuldfeq  45564  fmul01lt1lem1  45565  fmul01lt1lem2  45566  fprodexp  45575  fprodabs2  45576  fprodcnlem  45580  climmulf  45585  climexp  45586  climsuse  45589  climrecf  45590  climinff  45592  climaddf  45596  mullimc  45597  idlimc  45607  neglimc  45628  addlimc  45629  0ellimcdiv  45630  limclner  45632  climsubmpt  45641  climreclf  45645  climeldmeqmpt  45649  climfveqmpt  45652  fnlimfvre  45655  climfveqf  45661  climfveqmpt3  45663  climeldmeqf  45664  limsupref  45666  limsupbnd1f  45667  climeqf  45669  climeldmeqmpt3  45670  climinf2  45688  climinf2mpt  45695  climinfmpt  45696  limsupmnf  45702  limsupequz  45704  limsupre2  45706  limsupequzmptf  45712  limsupre3  45714  cncfshift  45855  fprodcncf  45881  dvmptmulf  45918  dvnmptdivc  45919  dvnmul  45924  dvmptfprodlem  45925  dvmptfprod  45926  iblspltprt  45954  stoweidlem3  45984  stoweidlem26  46007  stoweidlem31  46012  stoweidlem34  46015  stoweidlem42  46023  stoweidlem43  46024  stoweidlem48  46029  stoweidlem51  46032  stoweidlem59  46040  fourierdlem86  46173  fourierdlem89  46176  fourierdlem91  46178  fourierdlem112  46199  sge0f1o  46363  sge0lempt  46391  sge0iunmptlemfi  46394  sge0iunmptlemre  46396  sge0fodjrnlem  46397  sge0iunmpt  46399  sge0ltfirpmpt2  46407  sge0isummpt2  46413  sge0xaddlem2  46415  sge0xadd  46416  meadjiun  46447  voliunsge0lem  46453  meaiunincf  46464  meaiuninc3  46466  meaiininc  46468  hoimbl2  46646  vonhoire  46653  vonn0ioo2  46671  vonn0icc2  46673  salpreimagelt  46688  salpreimalegt  46690  salpreimagtge  46706  salpreimaltle  46707  salpreimagtlt  46711  2reu8i  47097  eu2ndop1stv  47109  f1oresf1o2  47275  ichnfimlem  47447  ichreuopeq  47457  reupr  47506  reuopreuprim  47510  2zrngmmgm  48236  nfsetrecs  49671  setrec2fun  49677  pgind  49702