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  bi3antOLD  289  pm2.67-2  402  pm3.41  559  pm3.42  560  jaob  781  3jaob  1281  merco1  1521  19.39  1716  r19.37  2968  axrep2  4506  dmcosseq  5202  fliftfun  6107  tz7.48lem  6999  ac6sfi  7660  frfi  7661  domunfican  7688  iunfi  7703  finsschain  7722  cantnfval2  7981  cantnflt  7984  cantnfval2OLD  8011  cantnfltOLD  8014  cnfcom  8037  cnfcomOLD  8045  kmlem1  8423  kmlem13  8435  axpowndlem2  8866  axpowndlem2OLD  8867  wunfi  8992  ingru  9086  xrub  11378  hashf1lem2  12320  caubnd  12957  fsum2d  13349  fsumabs  13375  fsumrlim  13385  fsumo1  13386  fsumiun  13395  ablfac1eulem  16687  mplcoe1  17660  mplcoe5  17664  mplcoe2OLD  17666  mdetunilem9  18551  t1t0  19077  fiuncmp  19132  ptcmpfi  19511  isfil2  19554  fsumcn  20571  ovolfiniun  21109  finiunmbl  21151  volfiniun  21154  itgfsum  21430  dvmptfsum  21573  pntrsumbnd  22941  nbgraf1olem1  23495  nmounbseqi  24322  nmounbseqiOLD  24323  isch3  24789  dmdmd  25849  mdslmd1lem2  25875  sumdmdi  25969  dmdbr4ati  25970  dmdbr6ati  25972  gsumle  26384  gsumvsca1  26389  gsumvsca2  26390  pwsiga  26711  fprod2d  27629  dfon2lem8  27740  meran1  28394  wl-syls2  28491  heibor1lem  28849  islinindfis  31093  4an4132  31506  con3ALT  31538  alrim3con13v  31542  bnj1533  32148  bnj110  32154  bnj1523  32365  bj-bi3ant  32418  bj-spnfw  32474  bj-spst  32481  bj-19.23bit  32483  bj-axrep2  32613  isltrn2N  34073  cdlemefrs32fva  34353
  Copyright terms: Public domain W3C validator