MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  imim1i 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  1484  19.39  1668  19.23hOLD  1829  ax12olem3OLD  1967  r19.37  2800  axrep2  4263  dmcosseq  5077  fliftfun  5973  tz7.48lem  6634  ac6sfi  7287  frfi  7288  domunfican  7315  iunfi  7330  finsschain  7348  cantnfval2  7557  cantnflt  7560  cnfcom  7590  kmlem1  7963  kmlem13  7975  axpowndlem2  8406  wunfi  8529  ingru  8623  xrub  10822  hashf1lem2  11632  caubnd  12089  fsum2d  12482  fsumabs  12507  fsumrlim  12517  fsumo1  12518  fsumiun  12527  ablfac1eulem  15557  mplcoe1  16455  mplcoe2  16457  t1t0  17334  fiuncmp  17389  ptcmpfi  17766  isfil2  17809  fsumcn  18771  ovolfiniun  19264  finiunmbl  19305  volfiniun  19308  itgfsum  19585  dvmptfsum  19726  pntrsumbnd  21127  nbgraf1olem1  21317  nmounbseqi  22126  nmounbseqiOLD  22127  isch3  22592  dmdmd  23651  mdslmd1lem2  23677  sumdmdi  23771  dmdbr4ati  23772  dmdbr6ati  23774  pwsiga  24309  dfon2lem8  25170  meran1  25875  wl-syls2  25930  heibor1lem  26209  con3ALT  27957  alrim3con13v  27960  bnj1533  28561  bnj110  28567  bnj1523  28778  ax12olem3aAUX7  28795  isltrn2N  30234  cdlemefrs32fva  30514
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator