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 1786 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 693	1 ⊢ Ⅎ𝑥(𝜑 → 𝜓)

Syntax hints:   → wi 4  Ⅎwnf 1785

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

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-nf 1786

This theorem is referenced by:  nfor  1906  nfia1  2159  nfnf1  2160  nfnf  2332  cbvsbvf  2368  mof  2564  cbvmow  2604  moexexlem  2627  cbvralfw  3278  cbvralf  3332  vtocl2gf  3529  vtocl3gf  3530  vtoclgaf  3533  vtocl2gaf  3536  vtocl2gafOLD  3537  vtocl3gaf  3538  vtocl3gafOLD  3539  rspct  3564  rspc  3566  ralab2  3657  mob  3677  reu2eqd  3696  reu8nf  3829  csbhypf  3879  cbvralcsf  3893  dfssf  3926  2reu4lem  4478  reusngf  4633  rexreusng  4638  reuprg0  4661  axrep2  5229  axrep3  5230  reusv2lem4  5348  reusv3  5352  iunopeqop  5477  nfpo  5546  nffr  5605  reuop  6259  frpoinsg  6309  fv3  6860  fvmptss  6962  fvmptd3f  6965  fvmptt  6970  fvmptf  6971  fmptco  7084  dff13f  7211  ovmpos  7516  ov2gf  7517  ovmpodf  7524  ov3  7531  tfisg  7806  tfis  7807  tfinds  7812  tfindes  7815  findes  7852  dfoprab4f  8010  offval22  8040  frpoins3xpg  8092  frpoins3xp3g  8093  tfr3  8340  dom2lem  8941  findcard2  9101  ac6sfi  9196  setinds  9670  frinsg  9675  dfac8clem  9954  aceq1  10039  dfac5lem5  10049  zfcndrep  10537  zfcndinf  10541  pwfseqlem4a  10584  pwfseqlem4  10585  uzind4s  12833  rabssnn0fi  13921  seqof2  13995  rlim2  15431  ello1mpt  15456  o1compt  15522  summolem2a  15650  sumss  15659  fsumclf  15673  fsumsplitf  15677  fsumsplit1  15680  o1fsum  15748  prodmolem2a  15869  fprodn0  15914  fproddivf  15922  fprodsplitf  15923  fprodsplit1f  15925  prmind2  16624  mreiincl  17527  gsumcom2  19916  gsummptnn0fz  19927  gsummoncoe1  22264  mdetralt2  22565  mdetunilem2  22569  ptcldmpt  23570  cnmptcom  23634  elmptrab  23783  isfildlem  23813  dvmptfsum  25947  dvfsumlem2  26001  dvfsumlem2OLD  26002  dvfsumlem4  26004  dvfsumrlim  26006  dvfsum2  26009  coeeq2  26215  dgrle  26216  rlimcnp  26943  lgamgulmlem2  27008  lgseisenlem2  27355  dchrisumlema  27467  dchrisumlem2  27469  dchrisumlem3  27470  nosupbnd1  27694  nosupbnd2  27696  noinfbnd1  27709  noinfbnd2  27711  mpteleeOLD  28980  gropd  29116  grstructd  29117  isch3  31329  atom1d  32441  mo5f  32575  ssiun2sf  32646  iinabrex  32656  ssrelf  32705  fmptcof2  32747  aciunf1lem  32752  nn0min  32912  fsumiunle  32921  esum2dlem  34270  fiunelros  34352  measiun  34396  bnj1385  35008  bnj1468  35022  bnj110  35034  bnj849  35101  bnj900  35105  bnj981  35126  bnj1014  35137  bnj1123  35162  bnj1128  35166  bnj1384  35208  bnj1489  35232  bnj1497  35236  subtr  36530  subtr2  36531  regsfromsetind  36691  currysetlem  37193  currysetlem1  37195  mptsnunlem  37593  finxpreclem2  37645  finxpreclem6  37651  ptrest  37870  poimirlem24  37895  poimirlem25  37896  poimirlem26  37897  poimirlem28  37899  fdc1  37997  ac6s6  38423  fsumshftd  39328  cdleme31sn1  40757  cdleme32fva  40813  cdlemk36  41289  eu6w  43034  fphpd  43173  monotuz  43298  monotoddzz  43300  oddcomabszz  43301  setindtrs  43382  aomclem6  43416  flcidc  43527  rababg  43930  ss2iundf  44015  binomcxplemnotnn0  44712  nfrelp  45305  uzwo4  45413  fiiuncl  45425  disjf1  45542  disjinfi  45551  dmrelrnrel  45584  supxrgere  45692  supxrgelem  45696  supxrge  45697  supxrleubrnmptf  45809  monoordxr  45840  monoord2xr  45842  fsummulc1f  45931  fsumnncl  45932  fsumf1of  45934  fsumiunss  45935  fsumreclf  45936  fsumlessf  45937  fsumsermpt  45939  fmul01  45940  fmuldfeqlem1  45942  fmuldfeq  45943  fmul01lt1lem1  45944  fmul01lt1lem2  45945  fprodexp  45954  fprodabs2  45955  fprodcnlem  45959  climmulf  45964  climexp  45965  climsuse  45968  climrecf  45969  climinff  45971  climaddf  45975  mullimc  45976  idlimc  45986  neglimc  46005  addlimc  46006  0ellimcdiv  46007  limclner  46009  climsubmpt  46018  climreclf  46022  climeldmeqmpt  46026  climfveqmpt  46029  fnlimfvre  46032  climfveqf  46038  climfveqmpt3  46040  climeldmeqf  46041  limsupref  46043  limsupbnd1f  46044  climeqf  46046  climeldmeqmpt3  46047  climinf2  46065  climinf2mpt  46072  climinfmpt  46073  limsupmnf  46079  limsupequz  46081  limsupre2  46083  limsupequzmptf  46089  limsupre3  46091  cncfshift  46232  fprodcncf  46258  dvmptmulf  46295  dvnmptdivc  46296  dvnmul  46301  dvmptfprodlem  46302  dvmptfprod  46303  iblspltprt  46331  stoweidlem3  46361  stoweidlem26  46384  stoweidlem31  46389  stoweidlem34  46392  stoweidlem42  46400  stoweidlem43  46401  stoweidlem48  46406  stoweidlem51  46409  stoweidlem59  46417  fourierdlem86  46550  fourierdlem89  46553  fourierdlem91  46555  fourierdlem112  46576  sge0f1o  46740  sge0lempt  46768  sge0iunmptlemfi  46771  sge0iunmptlemre  46773  sge0fodjrnlem  46774  sge0iunmpt  46776  sge0ltfirpmpt2  46784  sge0isummpt2  46790  sge0xaddlem2  46792  sge0xadd  46793  meadjiun  46824  voliunsge0lem  46830  meaiunincf  46841  meaiuninc3  46843  meaiininc  46845  hoimbl2  47023  vonhoire  47030  vonn0ioo2  47048  vonn0icc2  47050  salpreimagelt  47065  salpreimalegt  47067  salpreimagtge  47083  salpreimaltle  47084  salpreimagtlt  47088  2reu8i  47473  eu2ndop1stv  47485  f1oresf1o2  47651  ichnfimlem  47823  ichreuopeq  47833  reupr  47882  reuopreuprim  47886  2zrngmmgm  48612  nfsetrecs  50045  setrec2fun  50051  pgind  50076