MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  imim1i Unicode version

Theorem imim1i 54
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 19 . 2  |-  ( ch 
->  ch )
31, 2imim12i 53 1  |-  ( ( ps  ->  ch )  ->  ( ph  ->  ch ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4
This theorem is referenced by:  jarr  91  impt  149  jarl  155  bi3ant  280  pm2.67-2  391  pm3.41  542  pm3.42  543  jaob  758  3jaob  1244  merco1  1468  19.39  1672  19.23h  1728  ax12olem3  1870  r19.37  2689  axrep2  4133  dmcosseq  4946  fliftfun  5811  tz7.48lem  6453  ac6sfi  7101  frfi  7102  domunfican  7129  iunfi  7144  finsschain  7162  cantnfval2  7370  cantnflt  7373  cnfcom  7403  kmlem1  7776  kmlem13  7788  axpowndlem2  8220  wunfi  8343  ingru  8437  xrub  10630  hashf1lem2  11394  caubnd  11842  fsum2d  12234  fsumabs  12259  fsumrlim  12269  fsumo1  12270  fsumiun  12279  ablfac1eulem  15307  mplcoe1  16209  mplcoe2  16211  t1t0  17076  fiuncmp  17131  ptcmpfi  17504  isfil2  17551  fsumcn  18374  ovolfiniun  18860  finiunmbl  18901  volfiniun  18904  itgfsum  19181  dvmptfsum  19322  pntrsumbnd  20715  nmounbseqi  21355  nmounbseqiOLD  21356  isch3  21821  dmdmd  22880  mdslmd1lem2  22906  sumdmdi  23000  dmdbr4ati  23001  dmdbr6ati  23003  pwsiga  23491  dfon2lem8  24146  meran1  24850  wl-syls2  24905  domintrefb  25063  isconcl6a  26103  isconcl6ab  26104  isibg2a  26118  heibor1lem  26533  con3ALT  28293  alrim3con13v  28296  bnj1533  28884  bnj110  28890  bnj1523  29101  a12study  29132  isltrn2N  30309  cdlemefrs32fva  30589
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator