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  1290  merco1  1530  19.39  1725  19.21v  1930  r19.37  3010  axrep2  4560  dmcosseq  5264  fliftfun  6198  tz7.48lem  7106  ac6sfi  7764  frfi  7765  domunfican  7793  iunfi  7808  finsschain  7827  cantnfval2  8088  cantnflt  8091  cantnfval2OLD  8118  cantnfltOLD  8121  cnfcom  8144  cnfcomOLD  8152  kmlem1  8530  kmlem13  8542  axpowndlem2  8973  axpowndlem2OLD  8974  wunfi  9099  ingru  9193  xrub  11503  hashf1lem2  12471  caubnd  13154  fsum2d  13549  fsumabs  13578  fsumrlim  13588  fsumo1  13589  fsumiun  13598  ablfac1eulem  16925  mplcoe1  17926  mplcoe5  17930  mplcoe2OLD  17932  mdetunilem9  18917  t1t0  19643  fiuncmp  19698  ptcmpfi  20077  isfil2  20120  fsumcn  21137  ovolfiniun  21675  finiunmbl  21717  volfiniun  21720  itgfsum  21996  dvmptfsum  22139  pntrsumbnd  23507  nbgraf1olem1  24145  nmounbseqi  25396  nmounbseqiOLD  25397  isch3  25863  dmdmd  26923  mdslmd1lem2  26949  sumdmdi  27043  dmdbr4ati  27044  dmdbr6ati  27046  gsumle  27461  gsumvsca1  27464  gsumvsca2  27465  pwsiga  27798  fprod2d  28716  dfon2lem8  28827  meran1  29481  wl-syls2  29578  heibor1lem  29936  islinindfis  32149  4an4132  32365  con3ALT  32397  alrim3con13v  32401  bnj1533  33007  bnj110  33013  bnj1523  33224  bj-bi3ant  33277  bj-spnfw  33335  bj-spst  33342  bj-19.23bit  33344  bj-axrep2  33474  isltrn2N  34934  cdlemefrs32fva  35214  fiinfi  36796
  Copyright terms: Public domain W3C validator