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

Theorem imim1i 56
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 20 . 2  |-  ( ch 
->  ch )
31, 2imim12i 55 1  |-  ( ( ps  ->  ch )  ->  ( ph  ->  ch ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4
This theorem is referenced by:  jarr  93  impt  151  jarl  157  bi3ant  281  pm2.67-2  392  pm3.41  543  pm3.42  544  jaob  759  3jaob  1246  merco1  1487  19.39  1673  19.23hOLD  1839  ax12olem3OLD  2013  r19.37  2849  axrep2  4314  dmcosseq  5129  fliftfun  6026  tz7.48lem  6690  ac6sfi  7343  frfi  7344  domunfican  7371  iunfi  7386  finsschain  7405  cantnfval2  7614  cantnflt  7617  cnfcom  7647  kmlem1  8020  kmlem13  8032  axpowndlem2  8463  wunfi  8586  ingru  8680  xrub  10880  hashf1lem2  11695  caubnd  12152  fsum2d  12545  fsumabs  12570  fsumrlim  12580  fsumo1  12581  fsumiun  12590  ablfac1eulem  15620  mplcoe1  16518  mplcoe2  16520  t1t0  17402  fiuncmp  17457  ptcmpfi  17835  isfil2  17878  fsumcn  18890  ovolfiniun  19387  finiunmbl  19428  volfiniun  19431  itgfsum  19708  dvmptfsum  19849  pntrsumbnd  21250  nbgraf1olem1  21441  nmounbseqi  22268  nmounbseqiOLD  22269  isch3  22734  dmdmd  23793  mdslmd1lem2  23819  sumdmdi  23913  dmdbr4ati  23914  dmdbr6ati  23916  pwsiga  24503  fprod2d  25295  dfon2lem8  25405  meran1  26126  wl-syls2  26181  heibor1lem  26472  4an4132  28483  con3ALT  28515  alrim3con13v  28518  bnj1533  29124  bnj110  29130  bnj1523  29341  ax12olem3aAUX7  29358  isltrn2N  30818  cdlemefrs32fva  31098
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator