MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  imim1i Structured version   Unicode version

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  |-  ( ph  ->  ps )
Assertion
Ref Expression
imim1i  |-  ( ( ps  ->  ch )  ->  ( ph  ->  ch ) )

Proof of Theorem imim1i
StepHypRef Expression
1 imim1i.1 . 2  |-  ( ph  ->  ps )
2 id 22 . 2  |-  ( ch 
->  ch )
31, 2imim12i 57 1  |-  ( ( ps  ->  ch )  ->  ( ph  ->  ch ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7
This theorem is referenced by:  jarr  98  impt  157  jarl  163  pm2.67-2  400  pm3.41  557  pm3.42  558  jaob  781  3jaob  1288  merco1  1550  19.21v  1734  19.39  1762  r19.37  3003  axrep2  4552  dmcosseq  5253  fliftfun  6185  tz7.48lem  7098  ac6sfi  7756  frfi  7757  domunfican  7785  iunfi  7800  finsschain  7819  cantnfval2  8079  cantnflt  8082  cantnfval2OLD  8109  cantnfltOLD  8112  cnfcom  8135  cnfcomOLD  8143  kmlem1  8521  kmlem13  8533  axpowndlem2  8964  wunfi  9088  ingru  9182  xrub  11506  hashf1lem2  12489  caubnd  13273  fsum2d  13668  fsumabs  13697  fsumrlim  13707  fsumo1  13708  fsumiun  13717  fprod2d  13867  ablfac1eulem  17318  mplcoe1  18322  mplcoe5  18326  mplcoe2OLD  18328  mdetunilem9  19289  t1t0  20016  fiuncmp  20071  ptcmpfi  20480  isfil2  20523  fsumcn  21540  ovolfiniun  22078  finiunmbl  22120  volfiniun  22123  itgfsum  22399  dvmptfsum  22542  pntrsumbnd  23949  nbgraf1olem1  24643  nmounbseqi  25890  nmounbseqiALT  25891  isch3  26357  dmdmd  27417  mdslmd1lem2  27443  sumdmdi  27537  dmdbr4ati  27538  dmdbr6ati  27540  gsumle  28004  gsumvsca1  28008  gsumvsca2  28009  pwsiga  28360  dfon2lem8  29462  meran1  30104  wl-syls2  30205  heibor1lem  30545  islinindfis  33304  con3ALT  33687  alrim3con13v  33694  bnj1533  34311  bnj110  34317  bnj1523  34528  bj-bi3ant  34579  bj-spnfw  34632  bj-spst  34643  bj-19.23bit  34645  bj-axrep2  34776  isltrn2N  36241  cdlemefrs32fva  36523  fiinfi  38171
  Copyright terms: Public domain W3C validator