Theorem nfim 1893

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

Syntax hints:   → wi 4  Ⅎwnf 1779

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

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

This theorem is referenced by:  nfor  1901  nfia1  2150  nfnf1  2151  nfnf  2324  nfsbvOLD  2329  cbvsbvf  2363  mof  2560  cbvmow  2600  moexexlem  2623  cbvralfw  3301  cbvralf  3357  vtocl2gf  3571  vtocl3gf  3572  vtoclgaf  3575  vtocl2gaf  3578  vtocl2gafOLD  3579  vtocl3gaf  3580  vtocl3gafOLD  3581  rspct  3607  rspc  3609  ralab2  3705  mob  3725  reu2eqd  3744  reu8nf  3885  csbhypf  3936  cbvralcsf  3952  dfssf  3985  2reu4lem  4527  reusngf  4678  rexreusng  4683  reuprg0  4706  elintabOLD  4963  axrep2  5287  axrep3  5288  reusv2lem4  5406  reusv3  5410  iunopeqop  5530  nfpo  5602  nffr  5661  reuop  6314  frpoinsg  6365  wfisgOLD  6376  fv3  6924  fvmptss  7027  fvmptd3f  7030  fvmptt  7035  fvmptf  7036  fmptco  7148  dff13f  7275  ovmpos  7580  ov2gf  7581  ovmpodf  7588  ov3  7595  tfisg  7874  tfis  7875  tfinds  7880  tfindes  7883  findes  7922  dfoprab4f  8079  offval22  8111  frpoins3xpg  8163  frpoins3xp3g  8164  tfr3  8437  dom2lem  9030  findcard2  9202  ac6sfi  9317  frinsg  9788  dfac8clem  10069  aceq1  10154  dfac5lem5  10164  zfcndrep  10651  zfcndinf  10655  pwfseqlem4a  10698  pwfseqlem4  10699  uzind4s  12947  rabssnn0fi  14023  seqof2  14097  rlim2  15528  ello1mpt  15553  o1compt  15619  summolem2a  15747  sumss  15756  fsumclf  15770  fsumsplitf  15774  fsumsplit1  15777  o1fsum  15845  prodmolem2a  15966  fprodn0  16011  fproddivf  16019  fprodsplitf  16020  fprodsplit1f  16022  prmind2  16718  mreiincl  17640  gsumcom2  20007  gsummptnn0fz  20018  gsummoncoe1  22327  mdetralt2  22630  mdetunilem2  22634  ptcldmpt  23637  cnmptcom  23701  elmptrab  23850  isfildlem  23880  dvmptfsum  26027  dvfsumlem2  26081  dvfsumlem2OLD  26082  dvfsumlem4  26084  dvfsumrlim  26086  dvfsum2  26089  coeeq2  26295  dgrle  26296  rlimcnp  27022  lgamgulmlem2  27087  lgseisenlem2  27434  dchrisumlema  27546  dchrisumlem2  27548  dchrisumlem3  27549  nosupbnd1  27773  nosupbnd2  27775  noinfbnd1  27788  noinfbnd2  27790  mptelee  28924  gropd  29062  grstructd  29063  isch3  31269  atom1d  32381  mo5f  32516  ssiun2sf  32579  iinabrex  32588  ssrelf  32634  fmptcof2  32673  aciunf1lem  32678  nn0min  32826  fsumiunle  32835  esum2dlem  34072  fiunelros  34154  measiun  34198  bnj1385  34824  bnj1468  34838  bnj110  34850  bnj849  34917  bnj900  34921  bnj981  34942  bnj1014  34953  bnj1123  34978  bnj1128  34982  bnj1384  35024  bnj1489  35048  bnj1497  35052  setinds  35759  subtr  36296  subtr2  36297  currysetlem  36927  currysetlem1  36929  mptsnunlem  37320  finxpreclem2  37372  finxpreclem6  37378  ptrest  37605  poimirlem24  37630  poimirlem25  37631  poimirlem26  37632  poimirlem28  37634  fdc1  37732  ac6s6  38158  fsumshftd  38933  cdleme31sn1  40363  cdleme32fva  40419  cdlemk36  40895  eu6w  42662  fphpd  42803  monotuz  42929  monotoddzz  42931  oddcomabszz  42932  setindtrs  43013  aomclem6  43047  flcidc  43158  rababg  43563  ss2iundf  43648  binomcxplemnotnn0  44351  uzwo4  44992  fiiuncl  45004  disjf1  45125  disjinfi  45134  dmrelrnrel  45168  supxrgere  45282  supxrgelem  45286  supxrge  45287  supxrleubrnmptf  45400  monoordxr  45432  monoord2xr  45434  fsummulc1f  45526  fsumnncl  45527  fsumf1of  45529  fsumiunss  45530  fsumreclf  45531  fsumlessf  45532  fsumsermpt  45534  fmul01  45535  fmuldfeqlem1  45537  fmuldfeq  45538  fmul01lt1lem1  45539  fmul01lt1lem2  45540  fprodexp  45549  fprodabs2  45550  fprodcnlem  45554  climmulf  45559  climexp  45560  climsuse  45563  climrecf  45564  climinff  45566  climaddf  45570  mullimc  45571  idlimc  45581  neglimc  45602  addlimc  45603  0ellimcdiv  45604  limclner  45606  climsubmpt  45615  climreclf  45619  climeldmeqmpt  45623  climfveqmpt  45626  fnlimfvre  45629  climfveqf  45635  climfveqmpt3  45637  climeldmeqf  45638  limsupref  45640  limsupbnd1f  45641  climeqf  45643  climeldmeqmpt3  45644  climinf2  45662  climinf2mpt  45669  climinfmpt  45670  limsupmnf  45676  limsupequz  45678  limsupre2  45680  limsupequzmptf  45686  limsupre3  45688  cncfshift  45829  fprodcncf  45855  dvmptmulf  45892  dvnmptdivc  45893  dvnmul  45898  dvmptfprodlem  45899  dvmptfprod  45900  iblspltprt  45928  stoweidlem3  45958  stoweidlem26  45981  stoweidlem31  45986  stoweidlem34  45989  stoweidlem42  45997  stoweidlem43  45998  stoweidlem48  46003  stoweidlem51  46006  stoweidlem59  46014  fourierdlem86  46147  fourierdlem89  46150  fourierdlem91  46152  fourierdlem112  46173  sge0f1o  46337  sge0lempt  46365  sge0iunmptlemfi  46368  sge0iunmptlemre  46370  sge0fodjrnlem  46371  sge0iunmpt  46373  sge0ltfirpmpt2  46381  sge0isummpt2  46387  sge0xaddlem2  46389  sge0xadd  46390  meadjiun  46421  voliunsge0lem  46427  meaiunincf  46438  meaiuninc3  46440  meaiininc  46442  hoimbl2  46620  vonhoire  46627  vonn0ioo2  46645  vonn0icc2  46647  salpreimagelt  46662  salpreimalegt  46664  salpreimagtge  46680  salpreimaltle  46681  salpreimagtlt  46685  2reu8i  47062  eu2ndop1stv  47074  f1oresf1o2  47240  ichnfimlem  47387  ichreuopeq  47397  reupr  47446  reuopreuprim  47450  2zrngmmgm  48095  nfsetrecs  48916  setrec2fun  48922  pgind  48947