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  3276  cbvralf  3331  vtocl2gf  3535  vtocl3gf  3536  vtoclgaf  3539  vtocl2gaf  3542  vtocl2gafOLD  3543  vtocl3gaf  3544  vtocl3gafOLD  3545  rspct  3571  rspc  3573  ralab2  3665  mob  3685  reu2eqd  3704  reu8nf  3837  csbhypf  3887  cbvralcsf  3901  dfssf  3934  2reu4lem  4481  reusngf  4634  rexreusng  4639  reuprg0  4662  elintabOLD  4919  axrep2  5232  axrep3  5233  reusv2lem4  5351  reusv3  5355  iunopeqop  5476  nfpo  5545  nffr  5604  reuop  6254  frpoinsg  6304  fv3  6858  fvmptss  6962  fvmptd3f  6965  fvmptt  6970  fvmptf  6971  fmptco  7083  dff13f  7212  ovmpos  7517  ov2gf  7518  ovmpodf  7525  ov3  7532  tfisg  7810  tfis  7811  tfinds  7816  tfindes  7819  findes  7856  dfoprab4f  8014  offval22  8044  frpoins3xpg  8096  frpoins3xp3g  8097  tfr3  8344  dom2lem  8940  findcard2  9105  ac6sfi  9207  frinsg  9680  dfac8clem  9961  aceq1  10046  dfac5lem5  10056  zfcndrep  10543  zfcndinf  10547  pwfseqlem4a  10590  pwfseqlem4  10591  uzind4s  12843  rabssnn0fi  13927  seqof2  14001  rlim2  15438  ello1mpt  15463  o1compt  15529  summolem2a  15657  sumss  15666  fsumclf  15680  fsumsplitf  15684  fsumsplit1  15687  o1fsum  15755  prodmolem2a  15876  fprodn0  15921  fproddivf  15929  fprodsplitf  15930  fprodsplit1f  15932  prmind2  16631  mreiincl  17533  gsumcom2  19881  gsummptnn0fz  19892  gsummoncoe1  22171  mdetralt2  22472  mdetunilem2  22476  ptcldmpt  23477  cnmptcom  23541  elmptrab  23690  isfildlem  23720  dvmptfsum  25855  dvfsumlem2  25909  dvfsumlem2OLD  25910  dvfsumlem4  25912  dvfsumrlim  25914  dvfsum2  25917  coeeq2  26123  dgrle  26124  rlimcnp  26851  lgamgulmlem2  26916  lgseisenlem2  27263  dchrisumlema  27375  dchrisumlem2  27377  dchrisumlem3  27378  nosupbnd1  27602  nosupbnd2  27604  noinfbnd1  27617  noinfbnd2  27619  mptelee  28798  gropd  28934  grstructd  28935  isch3  31143  atom1d  32255  mo5f  32391  ssiun2sf  32461  iinabrex  32471  ssrelf  32516  fmptcof2  32554  aciunf1lem  32559  nn0min  32718  fsumiunle  32727  esum2dlem  34055  fiunelros  34137  measiun  34181  bnj1385  34795  bnj1468  34809  bnj110  34821  bnj849  34888  bnj900  34892  bnj981  34913  bnj1014  34924  bnj1123  34949  bnj1128  34953  bnj1384  34995  bnj1489  35019  bnj1497  35023  setinds  35739  subtr  36275  subtr2  36276  currysetlem  36906  currysetlem1  36908  mptsnunlem  37299  finxpreclem2  37351  finxpreclem6  37357  ptrest  37586  poimirlem24  37611  poimirlem25  37612  poimirlem26  37613  poimirlem28  37615  fdc1  37713  ac6s6  38139  fsumshftd  38918  cdleme31sn1  40348  cdleme32fva  40404  cdlemk36  40880  eu6w  42637  fphpd  42777  monotuz  42903  monotoddzz  42905  oddcomabszz  42906  setindtrs  42987  aomclem6  43021  flcidc  43132  rababg  43536  ss2iundf  43621  binomcxplemnotnn0  44318  nfrelp  44912  uzwo4  45020  fiiuncl  45032  disjf1  45150  disjinfi  45159  dmrelrnrel  45193  supxrgere  45302  supxrgelem  45306  supxrge  45307  supxrleubrnmptf  45420  monoordxr  45451  monoord2xr  45453  fsummulc1f  45542  fsumnncl  45543  fsumf1of  45545  fsumiunss  45546  fsumreclf  45547  fsumlessf  45548  fsumsermpt  45550  fmul01  45551  fmuldfeqlem1  45553  fmuldfeq  45554  fmul01lt1lem1  45555  fmul01lt1lem2  45556  fprodexp  45565  fprodabs2  45566  fprodcnlem  45570  climmulf  45575  climexp  45576  climsuse  45579  climrecf  45580  climinff  45582  climaddf  45586  mullimc  45587  idlimc  45597  neglimc  45618  addlimc  45619  0ellimcdiv  45620  limclner  45622  climsubmpt  45631  climreclf  45635  climeldmeqmpt  45639  climfveqmpt  45642  fnlimfvre  45645  climfveqf  45651  climfveqmpt3  45653  climeldmeqf  45654  limsupref  45656  limsupbnd1f  45657  climeqf  45659  climeldmeqmpt3  45660  climinf2  45678  climinf2mpt  45685  climinfmpt  45686  limsupmnf  45692  limsupequz  45694  limsupre2  45696  limsupequzmptf  45702  limsupre3  45704  cncfshift  45845  fprodcncf  45871  dvmptmulf  45908  dvnmptdivc  45909  dvnmul  45914  dvmptfprodlem  45915  dvmptfprod  45916  iblspltprt  45944  stoweidlem3  45974  stoweidlem26  45997  stoweidlem31  46002  stoweidlem34  46005  stoweidlem42  46013  stoweidlem43  46014  stoweidlem48  46019  stoweidlem51  46022  stoweidlem59  46030  fourierdlem86  46163  fourierdlem89  46166  fourierdlem91  46168  fourierdlem112  46189  sge0f1o  46353  sge0lempt  46381  sge0iunmptlemfi  46384  sge0iunmptlemre  46386  sge0fodjrnlem  46387  sge0iunmpt  46389  sge0ltfirpmpt2  46397  sge0isummpt2  46403  sge0xaddlem2  46405  sge0xadd  46406  meadjiun  46437  voliunsge0lem  46443  meaiunincf  46454  meaiuninc3  46456  meaiininc  46458  hoimbl2  46636  vonhoire  46643  vonn0ioo2  46661  vonn0icc2  46663  salpreimagelt  46678  salpreimalegt  46680  salpreimagtge  46696  salpreimaltle  46697  salpreimagtlt  46701  2reu8i  47087  eu2ndop1stv  47099  f1oresf1o2  47265  ichnfimlem  47437  ichreuopeq  47447  reupr  47496  reuopreuprim  47500  2zrngmmgm  48213  nfsetrecs  49648  setrec2fun  49654  pgind  49679