Theorem nfim 1900

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

Syntax hints:   → wi 4  Ⅎwnf 1787

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

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784  df-nf 1788

This theorem is referenced by:  nfor  1908  nfia1  2152  nfnf1  2153  nfnf  2324  nfsbvOLD  2329  cbval2vOLD  2343  sbievg  2361  mof  2563  cbvmow  2603  moexexlem  2628  nfabdwOLD  2930  cbvralfw  3358  cbvralfwOLD  3359  cbvralf  3361  vtocl2gf  3498  vtocl3gf  3499  vtoclgaf  3502  vtocl2gaf  3505  vtocl3gaf  3506  rspct  3537  rspc  3539  ralab2  3627  ralab2OLD  3628  mob  3647  reu2eqd  3666  reu8nf  3806  csbhypf  3857  cbvralcsf  3873  dfss2f  3907  rspn0OLD  4284  2reu4lem  4453  reusngf  4605  rexreusng  4612  reuprg0  4635  elintab  4887  axrep2  5208  axrep3  5209  reusv2lem4  5319  reusv3  5323  iunopeqop  5429  nfpo  5499  nffr  5554  reuop  6185  frpoinsg  6231  wfisgOLD  6242  fv3  6774  fvmptss  6869  fvmptd3f  6872  fvmptt  6877  fvmptf  6878  fmptco  6983  dff13f  7110  ovmpos  7399  ov2gf  7400  ovmpodf  7407  ov3  7413  tfis  7676  tfinds  7681  tfindes  7684  findes  7723  dfoprab4f  7869  offval22  7899  tfr3  8201  dom2lem  8735  findcard2  8909  findcard2OLD  8986  ac6sfi  8988  frinsg  9440  dfac8clem  9719  aceq1  9804  dfac5lem5  9814  zfcndrep  10301  zfcndinf  10305  pwfseqlem4a  10348  pwfseqlem4  10349  uzind4s  12577  rabssnn0fi  13634  seqof2  13709  rlim2  15133  ello1mpt  15158  o1compt  15224  summolem2a  15355  sumss  15364  fsumclf  15378  fsumsplitf  15382  fsumsplit1  15385  o1fsum  15453  prodmolem2a  15572  fprodn0  15617  fproddivf  15625  fprodsplitf  15626  fprodsplit1f  15628  prmind2  16318  mreiincl  17222  gsumcom2  19491  gsummptnn0fz  19502  gsummoncoe1  21385  mdetralt2  21666  mdetunilem2  21670  ptcldmpt  22673  cnmptcom  22737  elmptrab  22886  isfildlem  22916  dvmptfsum  25044  dvfsumlem2  25096  dvfsumlem4  25098  dvfsumrlim  25100  dvfsum2  25103  coeeq2  25308  dgrle  25309  rlimcnp  26020  lgamgulmlem2  26084  lgseisenlem2  26429  dchrisumlema  26541  dchrisumlem2  26543  dchrisumlem3  26544  mptelee  27166  gropd  27304  grstructd  27305  isch3  29504  atom1d  30616  mo5f  30738  ssiun2sf  30800  iinabrex  30809  ssrelf  30856  fmptcof2  30896  aciunf1lem  30901  nn0min  31036  fsumiunle  31045  esum2dlem  31960  fiunelros  32042  measiun  32086  bnj1385  32712  bnj1468  32726  bnj110  32738  bnj849  32805  bnj900  32809  bnj981  32830  bnj1014  32841  bnj1123  32866  bnj1128  32870  bnj1384  32912  bnj1489  32936  bnj1497  32940  setinds  33660  tfisg  33692  frpoins3xpg  33714  frpoins3xp3g  33715  nosupbnd1  33844  nosupbnd2  33846  noinfbnd1  33859  noinfbnd2  33861  subtr  34430  subtr2  34431  currysetlem  35061  currysetlem1  35063  mptsnunlem  35436  finxpreclem2  35488  finxpreclem6  35494  ptrest  35703  poimirlem24  35728  poimirlem25  35729  poimirlem26  35730  poimirlem28  35732  fdc1  35831  ac6s6  36257  fsumshftd  36893  cdleme31sn1  38322  cdleme32fva  38378  cdlemk36  38854  fphpd  40554  monotuz  40679  monotoddzz  40681  oddcomabszz  40682  setindtrs  40763  aomclem6  40800  flcidc  40915  rababg  41070  ss2iundf  41156  binomcxplemnotnn0  41863  uzwo4  42490  fiiuncl  42502  disjf1  42609  disjinfi  42620  dmrelrnrel  42654  supxrgere  42762  supxrgelem  42766  supxrge  42767  supxrleubrnmptf  42881  monoordxr  42913  monoord2xr  42915  fsummulc1f  43002  fsumnncl  43003  fsumf1of  43005  fsumiunss  43006  fsumreclf  43007  fsumlessf  43008  fsumsermpt  43010  fmul01  43011  fmuldfeqlem1  43013  fmuldfeq  43014  fmul01lt1lem1  43015  fmul01lt1lem2  43016  fprodexp  43025  fprodabs2  43026  fprodcnlem  43030  climmulf  43035  climexp  43036  climsuse  43039  climrecf  43040  climinff  43042  climaddf  43046  mullimc  43047  idlimc  43057  neglimc  43078  addlimc  43079  0ellimcdiv  43080  limclner  43082  climsubmpt  43091  climreclf  43095  climeldmeqmpt  43099  climfveqmpt  43102  fnlimfvre  43105  climfveqf  43111  climfveqmpt3  43113  climeldmeqf  43114  limsupref  43116  limsupbnd1f  43117  climeqf  43119  climeldmeqmpt3  43120  climinf2  43138  climinf2mpt  43145  climinfmpt  43146  limsupmnf  43152  limsupequz  43154  limsupre2  43156  limsupequzmptf  43162  limsupre3  43164  cncfshift  43305  fprodcncf  43331  dvmptmulf  43368  dvnmptdivc  43369  dvnmul  43374  dvmptfprodlem  43375  dvmptfprod  43376  iblspltprt  43404  stoweidlem3  43434  stoweidlem26  43457  stoweidlem31  43462  stoweidlem34  43465  stoweidlem42  43473  stoweidlem43  43474  stoweidlem48  43479  stoweidlem51  43482  stoweidlem59  43490  fourierdlem86  43623  fourierdlem89  43626  fourierdlem91  43628  fourierdlem112  43649  sge0f1o  43810  sge0lempt  43838  sge0iunmptlemfi  43841  sge0iunmptlemre  43843  sge0fodjrnlem  43844  sge0iunmpt  43846  sge0ltfirpmpt2  43854  sge0isummpt2  43860  sge0xaddlem2  43862  sge0xadd  43863  meadjiun  43894  voliunsge0lem  43900  meaiunincf  43911  meaiuninc3  43913  meaiininc  43915  hoimbl2  44093  vonhoire  44100  vonn0ioo2  44118  vonn0icc2  44120  salpreimagelt  44132  salpreimalegt  44134  salpreimagtge  44148  salpreimaltle  44149  salpreimagtlt  44153  2reu8i  44492  eu2ndop1stv  44504  f1oresf1o2  44670  ichnfimlem  44803  ichreuopeq  44813  reupr  44862  reuopreuprim  44866  2zrngmmgm  45392  nfsetrecs  46278  setrec2fun  46284