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

Theorem imim1i 60
Description: Inference adding common consequents in an implication, thereby interchanging the original antecedent and consequent. Inference associated with imim1 79. Its associated inference is syl 17. (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 59 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  101  impt  162  jarl  168  pm2.67-2  408  pm3.41  566  pm3.42  567  jaob  797  3jaob  1334  merco1  1600  19.21v  1790  19.21vOLDOLD  1791  19.39  1819  r19.37  2907  axrep2  4489  dmcosseq  5074  fliftfun  6191  tz7.48lem  7145  ac6sfi  7802  frfi  7803  domunfican  7831  iunfi  7849  finsschain  7868  cantnfval2  8161  cantnflt  8164  cnfcom  8192  kmlem1  8567  kmlem13  8579  axpowndlem2  9010  wunfi  9133  ingru  9227  xrub  11587  hashf1lem2  12614  caubnd  13432  fsum2d  13843  fsumabs  13872  fsumrlim  13882  fsumo1  13883  fsumiun  13892  fprod2d  14046  ablfac1eulem  17716  mplcoe1  18700  mplcoe5  18703  mdetunilem9  19656  t1t0  20375  fiuncmp  20430  ptcmpfi  20839  isfil2  20882  fsumcn  21913  ovolfiniun  22465  finiunmbl  22509  volfiniun  22512  itgfsum  22796  dvmptfsum  22939  pntrsumbnd  24416  nbgraf1olem1  25181  nmounbseqi  26430  nmounbseqiALT  26431  isch3  26906  dmdmd  27965  mdslmd1lem2  27991  sumdmdi  28085  dmdbr4ati  28086  dmdbr6ati  28088  gsumle  28549  gsumvsca1  28552  gsumvsca2  28553  pwsiga  28959  bnj1533  29669  bnj110  29675  bnj1523  29886  dfon2lem8  30442  meran1  31077  bj-bi3ant  31175  bj-ssbid2ALT  31261  bj-spnfw  31272  bj-spst  31284  bj-19.23bit  31286  bj-axrep2  31406  wl-syls2  31847  heibor1lem  32143  isltrn2N  33687  cdlemefrs32fva  33969  fiinfi  36179  con3ALT  36888  alrim3con13v  36895  islinindfis  40567
  Copyright terms: Public domain W3C validator