Theorem nfim 1931

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

This proof depends on syntax axioms:   → wi 4  Ⅎwnf 1816

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-nf 1817

This theorem is used by:  nfor  1939  nfia1  2193  nfnf1  2194  nfnf  2360  cbvsbvf  2395  mof  2591  cbvmow  2631  moexexlem  2654  cbvralfw  3306  cbvralf  3349  vtocl2gf  3535  vtocl3gf  3536  vtoclgaf  3539  vtocl2gaf  3542  vtocl3gaf  3543  rspct  3566  rspc  3568  ralab2  3658  mob  3678  reu2eqd  3697  reu8nf  3828  csbhypf  3879  cbvralcsf  3893  dfssf  3904  2reu4lem  4482  reusngf  4636  rexreusng  4641  reuprg0  4664  axrep2  5241  axrep3  5242  reusv2lem4  5370  reusv3  5374  iunopeqop  5501  iunopeqopOLD  5502  nfpo  5572  nffr  5631  reuop  6322  frpoinsg  6372  fv3  6934  fvmptss  7037  fvmptd3f  7040  fvmptt  7045  fvmptf  7046  fmptco  7162  dff13f  7290  ovmpos  7600  ov2gf  7601  ovmpodf  7608  ov3  7615  tfisg  7899  tfis  7900  tfinds  7905  tfindes  7908  findes  7946  dfoprab4f  8102  offval22  8134  frpoins3xpg  8194  frpoins3xp3g  8195  tfr3  8445  dom2lem  9057  findcard2  9218  ac6sfi  9313  setinds  9787  frinsg  9792  setrec2fun  10010  dfac8clem  10150  aceq1  10235  dfac5lem5  10245  zfcndrep  10738  zfcndinf  10742  pwfseqlem4a  10785  pwfseqlem4  10786  uzind4s  13075  rabssnn0fi  14169  seqof2  14243  rlim2  15707  ello1mpt  15732  o1compt  15798  summolem2a  15925  sumss  15934  fsumclf  15948  fsumsplitf  15952  fsumsplit1  15955  o1fsum  16024  prodmolem2a  16145  fprodn0  16190  fproddivf  16198  fprodsplitf  16199  fprodsplit1f  16201  prmind2  16904  mreiincl  17816  gsumcom2  20240  gsummptnn0fz  20251  gsummoncoe1  22681  mdetralt2  22979  mdetunilem2  22983  ptcldmpt  23988  cnmptcom  24052  elmptrab  24201  isfildlem  24231  dvmptfsum  26350  dvfsumlem2  26402  dvfsumlem4  26404  dvfsumrlim  26406  dvfsum2  26409  coeeq2  26616  dgrle  26617  rlimcnp  27350  lgamgulmlem2  27414  lgseisenlem2  27760  dchrisumlema  27872  dchrisumlem2  27874  dchrisumlem3  27875  nosupbnd1  28128  nosupbnd2  28130  noinfbnd1  28143  noinfbnd2  28145  mpteleeOLD  29530  gropd  29666  grstructd  29667  isch3  31900  atom1d  33012  mo5f  33184  ssiun2sf  33252  iinabrex  33261  ssrelf  33307  fmptcof2  33349  aciunf1lem  33354  nn0min  33508  fsumiunle  33516  esum2dlem  34835  fiunelros  34918  measiun  34962  bnj1385  35573  bnj1468  35587  bnj110  35599  bnj849  35666  bnj900  35670  bnj981  35691  bnj1014  35702  bnj1123  35727  bnj1128  35731  bnj1384  35773  bnj1489  35797  bnj1497  35801  subtr  37317  subtr2  37318  regsfromsetind  37542  currysetlem  38073  currysetlem1  38075  mptsnunlem  38529  finxpreclem2  38581  finxpreclem6  38587  ptrest  38805  poimirlem24  38830  poimirlem25  38831  poimirlem26  38832  poimirlem28  38834  fdc1  38946  ac6s6  39370  fsumshftd  40275  cdleme31sn1  41704  cdleme32fva  41760  cdlemk36  42236  eu6w  43953  fphpd  44089  monotuz  44214  monotoddzz  44216  oddcomabszz  44217  setindtrs  44298  aomclem6  44327  flcidc  44433  rababg  44836  ss2iundf  44920  binomcxplemnotnn0  45601  nfrelp  46203  uzwo4  46344  fiiuncl  46356  disjf1  46471  disjinfi  46480  dmrelrnrel  46512  supxrgere  46618  supxrgelem  46622  supxrge  46623  supxrleubrnmptf  46734  monoordxr  46765  monoord2xr  46767  fsummulc1f  46856  fsumnncl  46857  fsumf1of  46859  fsumiunss  46860  fsumreclf  46861  fsumlessf  46862  fsumsermpt  46864  fmul01  46865  fmuldfeqlem1  46867  fmuldfeq  46868  fmul01lt1lem1  46869  fmul01lt1lem2  46870  fprodexp  46879  fprodabs2  46880  fprodcnlem  46884  climmulf  46889  climexp  46890  climsuse  46893  climrecf  46894  climinff  46896  climaddf  46900  mullimc  46901  idlimc  46911  neglimc  46930  addlimc  46931  0ellimcdiv  46932  limclner  46934  climsubmpt  46943  climreclf  46947  climeldmeqmpt  46951  climfveqmpt  46954  fnlimfvre  46957  climfveqf  46963  climfveqmpt3  46965  climeldmeqf  46966  limsupref  46968  limsupbnd1f  46969  climeqf  46971  climeldmeqmpt3  46972  climinf2  46990  climinf2mpt  46997  climinfmpt  46998  limsupmnf  47004  limsupequz  47006  limsupre2  47008  limsupequzmptf  47014  limsupre3  47016  cncfshift  47157  fprodcncf  47183  dvmptmulf  47220  dvnmptdivc  47221  dvnmul  47226  dvmptfprodlem  47227  dvmptfprod  47228  iblspltprt  47256  stoweidlem3  47286  stoweidlem26  47309  stoweidlem31  47314  stoweidlem34  47317  stoweidlem42  47325  stoweidlem43  47326  stoweidlem48  47331  stoweidlem51  47334  stoweidlem59  47342  fourierdlem86  47475  fourierdlem89  47478  fourierdlem91  47480  fourierdlem112  47501  sge0f1o  47665  sge0lempt  47693  sge0iunmptlemfi  47696  sge0iunmptlemre  47698  sge0fodjrnlem  47699  sge0iunmpt  47701  sge0ltfirpmpt2  47709  sge0isummpt2  47715  sge0xaddlem2  47717  sge0xadd  47718  meadjiun  47749  voliunsge0lem  47755  meaiunincf  47766  meaiuninc3  47768  meaiininc  47770  hoimbl2  47948  vonhoire  47955  vonn0ioo2  47973  vonn0icc2  47975  salpreimagelt  47990  salpreimalegt  47992  salpreimagtge  48008  salpreimaltle  48009  salpreimagtlt  48013  2reu8i  48457  eu2ndop1stv  48468  f1oresf1o2  48634  ichnfimlem  48818  ichreuopeq  48828  reupr  48877  reuopreuprim  48881  2zrngmmgm  49622  nfsetrecs  51195  pgind  51216  nfals  51327  nfrals  51328  nfalseu  51358  nfralseu  51359