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, 5-Aug-1993.) (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  bi3antOLD  289  pm2.67-2  402  pm3.41  559  pm3.42  560  jaob  781  3jaob  1280  merco1  1520  19.39  1714  r19.37  2864  axrep2  4400  dmcosseq  5096  fliftfun  6000  tz7.48lem  6888  ac6sfi  7548  frfi  7549  domunfican  7576  iunfi  7591  finsschain  7610  cantnfval2  7869  cantnflt  7872  cantnfval2OLD  7899  cantnfltOLD  7902  cnfcom  7925  cnfcomOLD  7933  kmlem1  8311  kmlem13  8323  axpowndlem2  8754  axpowndlem2OLD  8755  wunfi  8880  ingru  8974  xrub  11266  hashf1lem2  12201  caubnd  12838  fsum2d  13230  fsumabs  13256  fsumrlim  13266  fsumo1  13267  fsumiun  13276  ablfac1eulem  16561  mplcoe1  17521  mplcoe2  17524  mplcoe2OLD  17525  mdetunilem9  18401  t1t0  18927  fiuncmp  18982  ptcmpfi  19361  isfil2  19404  fsumcn  20421  ovolfiniun  20959  finiunmbl  21000  volfiniun  21003  itgfsum  21279  dvmptfsum  21422  pntrsumbnd  22790  nbgraf1olem1  23301  nmounbseqi  24128  nmounbseqiOLD  24129  isch3  24595  dmdmd  25655  mdslmd1lem2  25681  sumdmdi  25775  dmdbr4ati  25776  dmdbr6ati  25778  gsumle  26197  gsumvsca1  26202  gsumvsca2  26203  pwsiga  26525  fprod2d  27443  dfon2lem8  27554  meran1  28209  wl-syls2  28301  heibor1lem  28661  islinindfis  30872  4an4132  31090  con3ALT  31122  alrim3con13v  31126  bnj1533  31732  bnj110  31738  bnj1523  31949  bj-bi3ant  31994  bj-spnfw  32050  bj-axrep2  32167  isltrn2N  33604  cdlemefrs32fva  33884
  Copyright terms: Public domain W3C validator