Theorem nfim 1916

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

Syntax hints:   → wi 4  Ⅎwnf 1803

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

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1800  df-nf 1804

This theorem is referenced by:  nfor  1924  nfia1  2187  nfnf1  2188  nfnf  2358  cbvsbvf  2394  mof  2590  cbvmow  2630  moexexlem  2653  cbvralfw  3302  cbvralf  3347  vtocl2gf  3536  vtocl3gf  3537  vtoclgaf  3540  vtocl2gaf  3543  vtocl3gaf  3544  rspct  3567  rspc  3569  ralab2  3660  mob  3680  reu2eqd  3699  reu8nf  3830  csbhypf  3880  cbvralcsf  3894  dfssf  3927  2reu4lem  4477  reusngf  4633  rexreusng  4638  reuprg0  4661  axrep2  5230  axrep3  5231  reusv2lem4  5358  reusv3  5362  iunopeqop  5490  iunopeqopOLD  5491  nfpo  5561  nffr  5620  reuop  6280  frpoinsg  6330  fv3  6885  fvmptss  6988  fvmptd3f  6991  fvmptt  6996  fvmptf  6997  fmptco  7111  dff13f  7239  ovmpos  7544  ov2gf  7545  ovmpodf  7552  ov3  7559  tfisg  7834  tfis  7835  tfinds  7840  tfindes  7843  findes  7881  dfoprab4f  8037  offval22  8067  frpoins3xpg  8120  frpoins3xp3g  8121  tfr3  8370  dom2lem  8973  findcard2  9133  ac6sfi  9228  setinds  9704  frinsg  9709  dfac8clem  9988  aceq1  10073  dfac5lem5  10083  zfcndrep  10572  zfcndinf  10576  pwfseqlem4a  10619  pwfseqlem4  10620  uzind4s  12909  rabssnn0fi  13999  seqof2  14073  rlim2  15523  ello1mpt  15548  o1compt  15614  summolem2a  15742  sumss  15751  fsumclf  15765  fsumsplitf  15769  fsumsplit1  15772  o1fsum  15841  prodmolem2a  15964  fprodn0  16009  fproddivf  16017  fprodsplitf  16018  fprodsplit1f  16020  prmind2  16719  mreiincl  17624  gsumcom2  20015  gsummptnn0fz  20026  gsummoncoe1  22368  mdetralt2  22666  mdetunilem2  22670  ptcldmpt  23671  cnmptcom  23735  elmptrab  23884  isfildlem  23914  dvmptfsum  26034  dvfsumlem2  26086  dvfsumlem4  26088  dvfsumrlim  26090  dvfsum2  26093  coeeq2  26299  dgrle  26300  rlimcnp  27027  lgamgulmlem2  27091  lgseisenlem2  27437  dchrisumlema  27549  dchrisumlem2  27551  dchrisumlem3  27552  nosupbnd1  27775  nosupbnd2  27777  noinfbnd1  27790  noinfbnd2  27792  mpteleeOLD  29093  gropd  29229  grstructd  29230  isch3  31441  atom1d  32553  mo5f  32685  ssiun2sf  32756  iinabrex  32766  ssrelf  32814  fmptcof2  32856  aciunf1lem  32861  nn0min  33020  fsumiunle  33028  esum2dlem  34386  fiunelros  34468  measiun  34512  bnj1385  35124  bnj1468  35138  bnj110  35150  bnj849  35217  bnj900  35221  bnj981  35242  bnj1014  35253  bnj1123  35278  bnj1128  35282  bnj1384  35324  bnj1489  35348  bnj1497  35352  subtr  36671  subtr2  36672  regsfromsetind  36896  currysetlem  37427  currysetlem1  37429  mptsnunlem  37829  finxpreclem2  37881  finxpreclem6  37887  ptrest  38115  poimirlem24  38140  poimirlem25  38141  poimirlem26  38142  poimirlem28  38144  fdc1  38242  ac6s6  38668  fsumshftd  39573  cdleme31sn1  41002  cdleme32fva  41058  cdlemk36  41534  eu6w  43255  fphpd  43390  monotuz  43515  monotoddzz  43517  oddcomabszz  43518  setindtrs  43599  aomclem6  43633  flcidc  43744  rababg  44147  ss2iundf  44232  binomcxplemnotnn0  44929  nfrelp  45522  uzwo4  45630  fiiuncl  45642  disjf1  45758  disjinfi  45767  dmrelrnrel  45799  supxrgere  45906  supxrgelem  45910  supxrge  45911  supxrleubrnmptf  46022  monoordxr  46053  monoord2xr  46055  fsummulc1f  46144  fsumnncl  46145  fsumf1of  46147  fsumiunss  46148  fsumreclf  46149  fsumlessf  46150  fsumsermpt  46152  fmul01  46153  fmuldfeqlem1  46155  fmuldfeq  46156  fmul01lt1lem1  46157  fmul01lt1lem2  46158  fprodexp  46167  fprodabs2  46168  fprodcnlem  46172  climmulf  46177  climexp  46178  climsuse  46181  climrecf  46182  climinff  46184  climaddf  46188  mullimc  46189  idlimc  46199  neglimc  46218  addlimc  46219  0ellimcdiv  46220  limclner  46222  climsubmpt  46231  climreclf  46235  climeldmeqmpt  46239  climfveqmpt  46242  fnlimfvre  46245  climfveqf  46251  climfveqmpt3  46253  climeldmeqf  46254  limsupref  46256  limsupbnd1f  46257  climeqf  46259  climeldmeqmpt3  46260  climinf2  46278  climinf2mpt  46285  climinfmpt  46286  limsupmnf  46292  limsupequz  46294  limsupre2  46296  limsupequzmptf  46302  limsupre3  46304  cncfshift  46445  fprodcncf  46471  dvmptmulf  46508  dvnmptdivc  46509  dvnmul  46514  dvmptfprodlem  46515  dvmptfprod  46516  iblspltprt  46544  stoweidlem3  46574  stoweidlem26  46597  stoweidlem31  46602  stoweidlem34  46605  stoweidlem42  46613  stoweidlem43  46614  stoweidlem48  46619  stoweidlem51  46622  stoweidlem59  46630  fourierdlem86  46763  fourierdlem89  46766  fourierdlem91  46768  fourierdlem112  46789  sge0f1o  46953  sge0lempt  46981  sge0iunmptlemfi  46984  sge0iunmptlemre  46986  sge0fodjrnlem  46987  sge0iunmpt  46989  sge0ltfirpmpt2  46997  sge0isummpt2  47003  sge0xaddlem2  47005  sge0xadd  47006  meadjiun  47037  voliunsge0lem  47043  meaiunincf  47054  meaiuninc3  47056  meaiininc  47058  hoimbl2  47236  vonhoire  47243  vonn0ioo2  47261  vonn0icc2  47263  salpreimagelt  47278  salpreimalegt  47280  salpreimagtge  47296  salpreimaltle  47297  salpreimagtlt  47301  2reu8i  47704  eu2ndop1stv  47716  f1oresf1o2  47882  ichnfimlem  48066  ichreuopeq  48076  reupr  48125  reuopreuprim  48129  2zrngmmgm  48871  nfsetrecs  50304  setrec2fun  50310  pgind  50335