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 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  160  jarl  166  pm2.67-2  403  pm3.41  561  pm3.42  562  jaob  790  3jaob  1326  merco1  1590  19.21v  1779  19.21vOLDOLD  1780  19.39  1808  r19.37  2974  axrep2  4538  dmcosseq  5115  fliftfun  6220  tz7.48lem  7169  ac6sfi  7824  frfi  7825  domunfican  7853  iunfi  7871  finsschain  7890  cantnfval2  8182  cantnflt  8185  cnfcom  8213  kmlem1  8587  kmlem13  8599  axpowndlem2  9030  wunfi  9153  ingru  9247  xrub  11604  hashf1lem2  12623  caubnd  13421  fsum2d  13831  fsumabs  13860  fsumrlim  13870  fsumo1  13871  fsumiun  13880  fprod2d  14034  ablfac1eulem  17704  mplcoe1  18688  mplcoe5  18691  mdetunilem9  19643  t1t0  20362  fiuncmp  20417  ptcmpfi  20826  isfil2  20869  fsumcn  21900  ovolfiniun  22452  finiunmbl  22495  volfiniun  22498  itgfsum  22782  dvmptfsum  22925  pntrsumbnd  24402  nbgraf1olem1  25167  nmounbseqi  26416  nmounbseqiALT  26417  isch3  26892  dmdmd  27951  mdslmd1lem2  27977  sumdmdi  28071  dmdbr4ati  28072  dmdbr6ati  28074  gsumle  28549  gsumvsca1  28553  gsumvsca2  28554  pwsiga  28960  bnj1533  29671  bnj110  29677  bnj1523  29888  dfon2lem8  30443  meran1  31076  bj-bi3ant  31177  bj-spnfw  31231  bj-spst  31242  bj-19.23bit  31244  bj-axrep2  31374  wl-syls2  31809  heibor1lem  32105  isltrn2N  33654  cdlemefrs32fva  33936  fiinfi  36147  con3ALT  36857  alrim3con13v  36864  islinindfis  39864
  Copyright terms: Public domain W3C validator