Theorem nfim 1897

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

Syntax hints:   → wi 4  Ⅎwnf 1784

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

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-nf 1785

This theorem is referenced by:  nfor  1905  nfia1  2156  nfnf1  2157  nfnf  2327  cbvsbvf  2363  mof  2558  cbvmow  2598  moexexlem  2621  cbvralfw  3272  cbvralf  3326  vtocl2gf  3523  vtocl3gf  3524  vtoclgaf  3527  vtocl2gaf  3530  vtocl2gafOLD  3531  vtocl3gaf  3532  vtocl3gafOLD  3533  rspct  3558  rspc  3560  ralab2  3651  mob  3671  reu2eqd  3690  reu8nf  3823  csbhypf  3873  cbvralcsf  3887  dfssf  3920  2reu4lem  4469  reusngf  4624  rexreusng  4629  reuprg0  4652  axrep2  5218  axrep3  5219  reusv2lem4  5337  reusv3  5341  iunopeqop  5459  nfpo  5528  nffr  5587  reuop  6240  frpoinsg  6290  fv3  6840  fvmptss  6941  fvmptd3f  6944  fvmptt  6949  fvmptf  6950  fmptco  7062  dff13f  7189  ovmpos  7494  ov2gf  7495  ovmpodf  7502  ov3  7509  tfisg  7784  tfis  7785  tfinds  7790  tfindes  7793  findes  7830  dfoprab4f  7988  offval22  8018  frpoins3xpg  8070  frpoins3xp3g  8071  tfr3  8318  dom2lem  8914  findcard2  9074  ac6sfi  9168  setinds  9639  frinsg  9644  dfac8clem  9923  aceq1  10008  dfac5lem5  10018  zfcndrep  10505  zfcndinf  10509  pwfseqlem4a  10552  pwfseqlem4  10553  uzind4s  12806  rabssnn0fi  13893  seqof2  13967  rlim2  15403  ello1mpt  15428  o1compt  15494  summolem2a  15622  sumss  15631  fsumclf  15645  fsumsplitf  15649  fsumsplit1  15652  o1fsum  15720  prodmolem2a  15841  fprodn0  15886  fproddivf  15894  fprodsplitf  15895  fprodsplit1f  15897  prmind2  16596  mreiincl  17498  gsumcom2  19887  gsummptnn0fz  19898  gsummoncoe1  22223  mdetralt2  22524  mdetunilem2  22528  ptcldmpt  23529  cnmptcom  23593  elmptrab  23742  isfildlem  23772  dvmptfsum  25906  dvfsumlem2  25960  dvfsumlem2OLD  25961  dvfsumlem4  25963  dvfsumrlim  25965  dvfsum2  25968  coeeq2  26174  dgrle  26175  rlimcnp  26902  lgamgulmlem2  26967  lgseisenlem2  27314  dchrisumlema  27426  dchrisumlem2  27428  dchrisumlem3  27429  nosupbnd1  27653  nosupbnd2  27655  noinfbnd1  27668  noinfbnd2  27670  mptelee  28873  gropd  29009  grstructd  29010  isch3  31221  atom1d  32333  mo5f  32468  ssiun2sf  32539  iinabrex  32549  ssrelf  32598  fmptcof2  32639  aciunf1lem  32644  nn0min  32803  fsumiunle  32812  esum2dlem  34105  fiunelros  34187  measiun  34231  bnj1385  34844  bnj1468  34858  bnj110  34870  bnj849  34937  bnj900  34941  bnj981  34962  bnj1014  34973  bnj1123  34998  bnj1128  35002  bnj1384  35044  bnj1489  35068  bnj1497  35072  subtr  36356  subtr2  36357  currysetlem  36987  currysetlem1  36989  mptsnunlem  37380  finxpreclem2  37432  finxpreclem6  37438  ptrest  37667  poimirlem24  37692  poimirlem25  37693  poimirlem26  37694  poimirlem28  37696  fdc1  37794  ac6s6  38220  fsumshftd  38999  cdleme31sn1  40428  cdleme32fva  40484  cdlemk36  40960  eu6w  42717  fphpd  42857  monotuz  42982  monotoddzz  42984  oddcomabszz  42985  setindtrs  43066  aomclem6  43100  flcidc  43211  rababg  43615  ss2iundf  43700  binomcxplemnotnn0  44397  nfrelp  44990  uzwo4  45098  fiiuncl  45110  disjf1  45228  disjinfi  45237  dmrelrnrel  45271  supxrgere  45380  supxrgelem  45384  supxrge  45385  supxrleubrnmptf  45497  monoordxr  45528  monoord2xr  45530  fsummulc1f  45619  fsumnncl  45620  fsumf1of  45622  fsumiunss  45623  fsumreclf  45624  fsumlessf  45625  fsumsermpt  45627  fmul01  45628  fmuldfeqlem1  45630  fmuldfeq  45631  fmul01lt1lem1  45632  fmul01lt1lem2  45633  fprodexp  45642  fprodabs2  45643  fprodcnlem  45647  climmulf  45652  climexp  45653  climsuse  45656  climrecf  45657  climinff  45659  climaddf  45663  mullimc  45664  idlimc  45674  neglimc  45693  addlimc  45694  0ellimcdiv  45695  limclner  45697  climsubmpt  45706  climreclf  45710  climeldmeqmpt  45714  climfveqmpt  45717  fnlimfvre  45720  climfveqf  45726  climfveqmpt3  45728  climeldmeqf  45729  limsupref  45731  limsupbnd1f  45732  climeqf  45734  climeldmeqmpt3  45735  climinf2  45753  climinf2mpt  45760  climinfmpt  45761  limsupmnf  45767  limsupequz  45769  limsupre2  45771  limsupequzmptf  45777  limsupre3  45779  cncfshift  45920  fprodcncf  45946  dvmptmulf  45983  dvnmptdivc  45984  dvnmul  45989  dvmptfprodlem  45990  dvmptfprod  45991  iblspltprt  46019  stoweidlem3  46049  stoweidlem26  46072  stoweidlem31  46077  stoweidlem34  46080  stoweidlem42  46088  stoweidlem43  46089  stoweidlem48  46094  stoweidlem51  46097  stoweidlem59  46105  fourierdlem86  46238  fourierdlem89  46241  fourierdlem91  46243  fourierdlem112  46264  sge0f1o  46428  sge0lempt  46456  sge0iunmptlemfi  46459  sge0iunmptlemre  46461  sge0fodjrnlem  46462  sge0iunmpt  46464  sge0ltfirpmpt2  46472  sge0isummpt2  46478  sge0xaddlem2  46480  sge0xadd  46481  meadjiun  46512  voliunsge0lem  46518  meaiunincf  46529  meaiuninc3  46531  meaiininc  46533  hoimbl2  46711  vonhoire  46718  vonn0ioo2  46736  vonn0icc2  46738  salpreimagelt  46753  salpreimalegt  46755  salpreimagtge  46771  salpreimaltle  46772  salpreimagtlt  46776  2reu8i  47152  eu2ndop1stv  47164  f1oresf1o2  47330  ichnfimlem  47502  ichreuopeq  47512  reupr  47561  reuopreuprim  47565  2zrngmmgm  48291  nfsetrecs  49726  setrec2fun  49732  pgind  49757