Theorem nfim 1898

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

Syntax hints:   → wi 4  Ⅎwnf 1786

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

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1783  df-nf 1787

This theorem is referenced by:  nfor  1906  nfia1  2155  nfnf1  2156  nfnf  2335  nfsbv  2339  nfsbvOLD  2340  cbval2vOLD  2354  cbval2OLD  2423  mof  2582  cbvmow  2623  moexexlem  2648  cbvabw  2828  nfabdw  2941  cbvralfw  3348  cbvralfwOLD  3349  cbvralf  3351  vtocl2gf  3489  vtocl3gf  3490  vtoclgaf  3492  vtocl2gaf  3495  vtocl3gaf  3496  rspct  3528  rspc  3530  ralab2  3612  ralab2OLD  3613  mob  3632  reu2eqd  3651  reu8nf  3784  csbhypf  3834  cbvralcsf  3848  vtocl2dOLD  3854  dfss2f  3883  rspn0OLD  4253  2reu4lem  4419  reusngf  4570  rexreusng  4575  reuprg0  4596  elintab  4850  axrep2  5160  axrep3  5161  reusv2lem4  5271  reusv3  5275  iunopeqop  5381  nfpo  5449  nffr  5499  reuop  6123  wfisg  6162  fv3  6677  fvmptss  6772  fvmptd3f  6775  fvmptt  6780  fvmptf  6781  fmptco  6883  dff13f  7007  ovmpos  7294  ov2gf  7295  ovmpodf  7302  ov3  7308  tfis  7569  tfinds  7574  tfindes  7577  findes  7613  dfoprab4f  7759  offval22  7789  tfr3  8046  dom2lem  8568  findcard2  8783  findcard2OLD  8784  ac6sfi  8788  dfac8clem  9485  aceq1  9570  dfac5lem5  9580  zfcndrep  10067  zfcndinf  10071  pwfseqlem4a  10114  pwfseqlem4  10115  uzind4s  12341  rabssnn0fi  13396  seqof2  13471  rlim2  14894  ello1mpt  14919  o1compt  14985  summolem2a  15113  sumss  15122  fsumsplitf  15139  o1fsum  15209  prodmolem2a  15329  fprodn0  15374  fproddivf  15382  fprodsplitf  15383  fprodsplit1f  15385  prmind2  16074  mreiincl  16918  gsumcom2  19156  gsummptnn0fz  19167  gsummoncoe1  21021  mdetralt2  21302  mdetunilem2  21306  ptcldmpt  22307  cnmptcom  22371  elmptrab  22520  isfildlem  22550  dvmptfsum  24667  dvfsumlem2  24719  dvfsumlem4  24721  dvfsumrlim  24723  dvfsum2  24726  coeeq2  24931  dgrle  24932  rlimcnp  25643  lgamgulmlem2  25707  lgseisenlem2  26052  dchrisumlema  26164  dchrisumlem2  26166  dchrisumlem3  26167  mptelee  26781  gropd  26916  grstructd  26917  isch3  29116  atom1d  30228  mo5f  30352  ssiun2sf  30414  iinabrex  30423  ssrelf  30470  fmptcof2  30511  aciunf1lem  30516  nn0min  30651  fsumiunle  30660  esum2dlem  31572  fiunelros  31654  measiun  31698  bnj1385  32325  bnj1468  32339  bnj110  32351  bnj849  32418  bnj900  32422  bnj981  32443  bnj1014  32454  bnj1123  32479  bnj1128  32483  bnj1384  32525  bnj1489  32549  bnj1497  32553  setinds  33263  tfisg  33295  frpoinsg  33321  frpoins3xpg  33325  frpoins3xp3g  33326  frinsg  33330  nosupbnd1  33475  nosupbnd2  33477  noinfbnd1  33490  noinfbnd2  33492  subtr  34045  subtr2  34046  currysetlem  34654  currysetlem1  34656  mptsnunlem  35028  finxpreclem2  35080  finxpreclem6  35086  ptrest  35329  poimirlem24  35354  poimirlem25  35355  poimirlem26  35356  poimirlem28  35358  fdc1  35457  ac6s6  35883  fsumshftd  36521  cdleme31sn1  37950  cdleme32fva  38006  cdlemk36  38482  fphpd  40123  monotuz  40248  monotoddzz  40250  oddcomabszz  40251  setindtrs  40332  aomclem6  40369  flcidc  40484  rababg  40639  ss2iundf  40726  binomcxplemnotnn0  41426  uzwo4  42053  fiiuncl  42065  disjf1  42172  disjinfi  42183  dmrelrnrel  42217  supxrgere  42326  supxrgelem  42330  supxrge  42331  supxrleubrnmptf  42449  monoordxr  42481  monoord2xr  42483  fsumclf  42570  fsummulc1f  42571  fsumnncl  42572  fsumsplit1  42573  fsumf1of  42575  fsumiunss  42576  fsumreclf  42577  fsumlessf  42578  fsumsermpt  42580  fmul01  42581  fmuldfeqlem1  42583  fmuldfeq  42584  fmul01lt1lem1  42585  fmul01lt1lem2  42586  fprodexp  42595  fprodabs2  42596  fprodcnlem  42600  climmulf  42605  climexp  42606  climsuse  42609  climrecf  42610  climinff  42612  climaddf  42616  mullimc  42617  idlimc  42627  neglimc  42648  addlimc  42649  0ellimcdiv  42650  limclner  42652  climsubmpt  42661  climreclf  42665  climeldmeqmpt  42669  climfveqmpt  42672  fnlimfvre  42675  climfveqf  42681  climfveqmpt3  42683  climeldmeqf  42684  limsupref  42686  limsupbnd1f  42687  climeqf  42689  climeldmeqmpt3  42690  climinf2  42708  climinf2mpt  42715  climinfmpt  42716  limsupmnf  42722  limsupequz  42724  limsupre2  42726  limsupequzmptf  42732  limsupre3  42734  cncfshift  42875  fprodcncf  42901  dvmptmulf  42938  dvnmptdivc  42939  dvnmul  42944  dvmptfprodlem  42945  dvmptfprod  42946  iblspltprt  42974  stoweidlem3  43004  stoweidlem26  43027  stoweidlem31  43032  stoweidlem34  43035  stoweidlem42  43043  stoweidlem43  43044  stoweidlem48  43049  stoweidlem51  43052  stoweidlem59  43060  fourierdlem86  43193  fourierdlem89  43196  fourierdlem91  43198  fourierdlem112  43219  sge0f1o  43380  sge0lempt  43408  sge0iunmptlemfi  43411  sge0iunmptlemre  43413  sge0fodjrnlem  43414  sge0iunmpt  43416  sge0ltfirpmpt2  43424  sge0isummpt2  43430  sge0xaddlem2  43432  sge0xadd  43433  meadjiun  43464  voliunsge0lem  43470  meaiunincf  43481  meaiuninc3  43483  meaiininc  43485  hoimbl2  43663  vonhoire  43670  vonn0ioo2  43688  vonn0icc2  43690  salpreimagelt  43702  salpreimalegt  43704  salpreimagtge  43718  salpreimaltle  43719  salpreimagtlt  43723  2reu8i  44030  eu2ndop1stv  44042  f1oresf1o2  44208  ichnfimlem  44341  ichreuopeq  44351  reupr  44400  reuopreuprim  44404  2zrngmmgm  44930  nfsetrecs  45600  setrec2fun  45606