MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  imim1i Structured 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 23 . 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  160  jarl  166  pm2.67-2  403  pm3.41  561  pm3.42  562  jaob  790  3jaob  1326  merco1  1592  19.21v  1778  19.21vOLDOLD  1779  19.39  1807  r19.37  2984  axrep2  4540  dmcosseq  5116  fliftfun  6220  tz7.48lem  7166  ac6sfi  7821  frfi  7822  domunfican  7850  iunfi  7868  finsschain  7887  cantnfval2  8173  cantnflt  8176  cnfcom  8204  kmlem1  8578  kmlem13  8590  axpowndlem2  9021  wunfi  9145  ingru  9239  xrub  11597  hashf1lem2  12614  caubnd  13400  fsum2d  13810  fsumabs  13839  fsumrlim  13849  fsumo1  13850  fsumiun  13859  fprod2d  14013  ablfac1eulem  17640  mplcoe1  18624  mplcoe5  18627  mdetunilem9  19576  t1t0  20295  fiuncmp  20350  ptcmpfi  20759  isfil2  20802  fsumcn  21798  ovolfiniun  22332  finiunmbl  22374  volfiniun  22377  itgfsum  22661  dvmptfsum  22804  pntrsumbnd  24267  nbgraf1olem1  25014  nmounbseqi  26263  nmounbseqiALT  26264  isch3  26729  dmdmd  27788  mdslmd1lem2  27814  sumdmdi  27908  dmdbr4ati  27909  dmdbr6ati  27911  gsumle  28380  gsumvsca1  28384  gsumvsca2  28385  pwsiga  28791  bnj1533  29451  bnj110  29457  bnj1523  29668  dfon2lem8  30223  meran1  30856  bj-bi3ant  30957  bj-spnfw  31011  bj-spst  31022  bj-19.23bit  31024  bj-axrep2  31155  wl-syls2  31552  heibor1lem  31845  isltrn2N  33394  cdlemefrs32fva  33676  fiinfi  35876  con3ALT  36524  alrim3con13v  36531  islinindfis  39002
  Copyright terms: Public domain W3C validator