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, 5-Aug-1993.) (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  554  pm3.42  555  jaob  774  3jaob  1273  merco1  1523  19.39  1713  r19.37  2859  axrep2  4393  dmcosseq  5088  fliftfun  5992  tz7.48lem  6882  ac6sfi  7544  frfi  7545  domunfican  7572  iunfi  7587  finsschain  7606  cantnfval2  7865  cantnflt  7868  cantnfval2OLD  7895  cantnfltOLD  7898  cnfcom  7921  cnfcomOLD  7929  kmlem1  8307  kmlem13  8319  axpowndlem2  8750  axpowndlem2OLD  8751  wunfi  8875  ingru  8969  xrub  11261  hashf1lem2  12192  caubnd  12829  fsum2d  13221  fsumabs  13246  fsumrlim  13256  fsumo1  13257  fsumiun  13266  ablfac1eulem  16546  mplcoe1  17477  mplcoe2  17480  mplcoe2OLD  17481  mdetunilem9  18267  t1t0  18793  fiuncmp  18848  ptcmpfi  19227  isfil2  19270  fsumcn  20287  ovolfiniun  20825  finiunmbl  20866  volfiniun  20869  itgfsum  21145  dvmptfsum  21288  pntrsumbnd  22699  nbgraf1olem1  23172  nmounbseqi  23999  nmounbseqiOLD  24000  isch3  24466  dmdmd  25526  mdslmd1lem2  25552  sumdmdi  25646  dmdbr4ati  25647  dmdbr6ati  25649  gsumle  26097  gsumvsca1  26103  gsumvsca2  26104  pwsiga  26426  fprod2d  27338  dfon2lem8  27449  meran1  28104  wl-syls2  28196  heibor1lem  28549  islinindfis  30689  4an4132  30901  con3ALT  30933  alrim3con13v  30937  bnj1533  31544  bnj110  31550  bnj1523  31761  bj-bi3ant  31774  bj-spnfw  31826  bj-axrep2  31927  isltrn2N  33334  cdlemefrs32fva  33614
  Copyright terms: Public domain W3C validator