Theorem imim1i 58

Description: Inference adding common consequents in an implication, thereby interchanging the original antecedent and consequent. (Contributed by NM, 28-Dec-1992.) (Proof shortened by Wolf Lammen, 4-Aug-2012.)

Hypothesis

Ref	Expression
imim1i.1

Assertion

Ref	Expression
imim1i

Proof of Theorem imim1i

Step	Hyp	Ref	Expression
1		imim1i.1	. 2
2		id 22	. 2
3	1, 2	imim12i 57	1

Syntax hints:  ->wi 4

This theorem is referenced by:  jarr  98  impt  157  jarl  163  bi3antOLD  289  pm2.67-2  402  pm3.41  559  pm3.42  560  jaob  783  3jaob  1290  merco1  1546  19.21v  1729  19.39  1757  r19.37  3006  axrep2  4565  dmcosseq  5269  fliftfun  6210  tz7.48lem  7125  ac6sfi  7784  frfi  7785  domunfican  7813  iunfi  7828  finsschain  7847  cantnfval2  8109  cantnflt  8112  cantnfval2OLD  8139  cantnfltOLD  8142  cnfcom  8165  cnfcomOLD  8173  kmlem1  8551  kmlem13  8563  axpowndlem2  8994  axpowndlem2OLD  8995  wunfi  9120  ingru  9214  xrub  11532  hashf1lem2  12505  caubnd  13191  fsum2d  13586  fsumabs  13615  fsumrlim  13625  fsumo1  13626  fsumiun  13635  fprod2d  13785  ablfac1eulem  17123  mplcoe1  18127  mplcoe5  18131  mplcoe2OLD  18133  mdetunilem9  19122  t1t0  19849  fiuncmp  19904  ptcmpfi  20314  isfil2  20357  fsumcn  21374  ovolfiniun  21912  finiunmbl  21954  volfiniun  21957  itgfsum  22233  dvmptfsum  22376  pntrsumbnd  23751  nbgraf1olem1  24441  nmounbseqi  25692  nmounbseqiOLD  25693  isch3  26159  dmdmd  27219  mdslmd1lem2  27245  sumdmdi  27339  dmdbr4ati  27340  dmdbr6ati  27342  gsumle  27770  gsumvsca1  27773  gsumvsca2  27774  pwsiga  28130  dfon2lem8  29222  meran1  29876  wl-syls2  29973  heibor1lem  30305  islinindfis  33050  con3ALT  33300  alrim3con13v  33304  bnj1533  33910  bnj110  33916  bnj1523  34127  bj-bi3ant  34178  bj-spnfw  34231  bj-spst  34242  bj-19.23bit  34244  bj-axrep2  34375  isltrn2N  35844  cdlemefrs32fva  36126  fiinfi  37758

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7