Theorem nfim 1813

Description: If 𝑥 is not free in 𝜑 and 𝜓, it is not free in (𝜑 → 𝜓). (Contributed by Mario Carneiro, 11-Aug-2016.) (Proof shortened by Wolf Lammen, 2-Jan-2018.) df-nf 1701 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	. . . 4 ⊢ Ⅎ𝑥𝜑
2	1	a1i 11	. . 3 ⊢ (⊤ → Ⅎ𝑥𝜑)
3		nfim.2	. . . 4 ⊢ Ⅎ𝑥𝜓
4	3	a1i 11	. . 3 ⊢ (⊤ → Ⅎ𝑥𝜓)
5	2, 4	nfimd 1812	. 2 ⊢ (⊤ → Ⅎ𝑥(𝜑 → 𝜓))
6	5	trud 1484	1 ⊢ Ⅎ𝑥(𝜑 → 𝜓)

Syntax hints:   → wi 4  ⊤wtru 1476  Ⅎwnf 1699

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

This theorem depends on definitions:  df-bi 196  df-or 384  df-tru 1478  df-ex 1696  df-nf 1701

This theorem is referenced by:  nfanOLD  1817  nfor  1822  nfia1  2017  nfnf1  2018  nfnf  2144  cbval2  2267  mo2  2467  nfmo1  2469  moexex  2529  cbvralf  3141  vtocl2gf  3241  vtocl3gf  3242  vtoclgaf  3244  vtocl2gaf  3246  vtocl3gaf  3248  rspct  3275  rspc  3276  ralab2  3338  mob  3355  reu2eqd  3370  csbhypf  3518  cbvralcsf  3531  dfss2f  3559  rspn0  3892  elintab  4422  axrep2  4701  axrep3  4702  reusv2lem4  4798  reusv3  4802  iunopeqop  4906  nfpo  4964  nffr  5012  wfisg  5632  fv3  6116  tz6.12c  6123  fvmptss  6201  fvmptdf  6204  fvmptt  6208  fvmptf  6209  fmptco  6303  dff13f  6417  ovmpt2s  6682  ov2gf  6683  ovmpt2df  6690  ov3  6695  tfis  6946  tfinds  6951  tfindes  6954  findes  6988  dfoprab4f  7117  offval22  7140  tfr3  7382  dom2lem  7881  findcard2  8085  ac6sfi  8089  dfac8clem  8738  aceq1  8823  dfac5lem5  8833  zfcndrep  9315  zfcndinf  9319  pwfseqlem4a  9362  pwfseqlem4  9363  uzind4s  11624  rabssnn0fi  12647  seqof2  12721  rlim2  14075  ello1mpt  14100  o1compt  14166  summolem2a  14293  sumss  14302  o1fsum  14386  prodmolem2a  14503  fprodn0  14548  fproddivf  14557  fprodsplitf  14558  fprodsplit1f  14560  prmind2  15236  mreiincl  16079  gsumcom2  18197  gsummptnn0fz  18205  gsummoncoe1  19495  mdetralt2  20234  mdetunilem2  20238  ptcldmpt  21227  cnmptcom  21291  elmptrab  21440  isfildlem  21471  dvmptfsum  23542  dvfsumlem2  23594  dvfsumlem4  23596  dvfsumrlim  23598  dvfsum2  23601  coeeq2  23802  dgrle  23803  rlimcnp  24492  lgamgulmlem2  24556  lgseisenlem2  24901  dchrisumlema  24977  dchrisumlem2  24979  dchrisumlem3  24980  mptelee  25575  gropd  25708  grstructd  25709  isch3  27482  atom1d  28596  vtocl2d  28699  mo5f  28708  ssiun2sf  28760  ssrelf  28805  fmptcof2  28839  aciunf1lem  28844  nn0min  28954  esum2dlem  29481  fiunelros  29564  measiun  29608  bnj1385  30157  bnj1468  30170  bnj110  30182  bnj849  30249  bnj900  30253  bnj981  30274  bnj1014  30284  bnj1123  30308  bnj1128  30312  bnj1384  30354  bnj1489  30378  bnj1497  30382  setinds  30927  tfisg  30960  frinsg  30986  subtr  31478  subtr2  31479  bj-cbval2v  31924  bj-axrep2  31977  bj-axrep3  31978  bj-mo3OLD  32022  mptsnunlem  32361  finxpreclem2  32403  finxpreclem6  32409  ptrest  32578  poimirlem24  32603  poimirlem25  32604  poimirlem26  32605  poimirlem28  32607  fdc1  32712  ac6s6  33150  fsumshftd  33255  fsumshftdOLD  33256  cdleme31sn1  34687  cdleme32fva  34743  cdlemk36  35219  fphpd  36398  monotuz  36524  monotoddzz  36526  oddcomabszz  36527  setindtrs  36610  aomclem6  36647  flcidc  36763  rababg  36898  ss2iundf  36970  binomcxplemnotnn0  37577  uzwo4  38246  fiiuncl  38259  disjf1  38364  disjinfi  38375  dmrelrnrel  38414  supxrgere  38490  supxrgelem  38494  supxrge  38495  fsumclf  38633  fsumsplitf  38634  fsummulc1f  38635  fsumnncl  38638  fsumsplit1  38639  fsumf1of  38641  fsumiunss  38642  fsumreclf  38643  fsumlessf  38644  fsumsermpt  38646  fmul01  38647  fmuldfeqlem1  38649  fmuldfeq  38650  fmul01lt1lem1  38651  fmul01lt1lem2  38652  fprodexp  38661  fprodabs2  38662  fprodcnlem  38666  climmulf  38671  climexp  38672  climsuse  38675  climrecf  38676  climinff  38678  climaddf  38682  mullimc  38683  idlimc  38693  neglimc  38714  addlimc  38715  0ellimcdiv  38716  limclner  38718  climsubmpt  38727  climreclf  38731  climeldmeqmpt  38735  climfveqmpt  38738  fnlimfvre  38741  cncfshift  38759  cncfiooicclem1  38779  fprodcncf  38787  dvmptmulf  38827  dvnmptdivc  38828  dvnmul  38833  dvmptfprodlem  38834  dvmptfprod  38835  iblspltprt  38865  stoweidlem3  38896  stoweidlem26  38919  stoweidlem31  38924  stoweidlem34  38927  stoweidlem42  38935  stoweidlem43  38936  stoweidlem48  38941  stoweidlem51  38944  stoweidlem59  38952  fourierdlem86  39085  fourierdlem89  39088  fourierdlem91  39090  fourierdlem112  39111  sge0f1o  39275  sge0lempt  39303  sge0iunmptlemfi  39306  sge0iunmptlemre  39308  sge0fodjrnlem  39309  sge0iunmpt  39311  sge0ltfirpmpt2  39319  sge0isummpt2  39325  sge0xaddlem2  39327  sge0xadd  39328  meadjiun  39359  voliunsge0lem  39365  meaiininc  39377  hoimbl2  39555  vonhoire  39563  vonn0ioo2  39581  vonn0icc2  39583  salpreimagelt  39595  salpreimalegt  39597  salpreimagtge  39611  salpreimaltle  39612  salpreimagtlt  39616  2reu4a  39838  eu2ndop1stv  39851  2zrngmmgm  41736  nfsetrecs  42232  setrec2fun  42238