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  1650  19.23h  1740  ax12olem3  1882  r19.37  2702  axrep2  4149  dmcosseq  4962  fliftfun  5827  tz7.48lem  6469  ac6sfi  7117  frfi  7118  domunfican  7145  iunfi  7160  finsschain  7178  cantnfval2  7386  cantnflt  7389  cnfcom  7419  kmlem1  7792  kmlem13  7804  axpowndlem2  8236  wunfi  8359  ingru  8453  xrub  10646  hashf1lem2  11410  caubnd  11858  fsum2d  12250  fsumabs  12275  fsumrlim  12285  fsumo1  12286  fsumiun  12295  ablfac1eulem  15323  mplcoe1  16225  mplcoe2  16227  t1t0  17092  fiuncmp  17147  ptcmpfi  17520  isfil2  17567  fsumcn  18390  ovolfiniun  18876  finiunmbl  18917  volfiniun  18920  itgfsum  19197  dvmptfsum  19338  pntrsumbnd  20731  nmounbseqi  21371  nmounbseqiOLD  21372  isch3  21837  dmdmd  22896  mdslmd1lem2  22922  sumdmdi  23016  dmdbr4ati  23017  dmdbr6ati  23019  pwsiga  23506  dfon2lem8  24217  meran1  24922  wl-syls2  24977  domintrefb  25166  isconcl6a  26206  isconcl6ab  26207  isibg2a  26221  heibor1lem  26636  con3ALT  28592  alrim3con13v  28595  bnj1533  29200  bnj110  29206  bnj1523  29417  ax12olem3aAUX7  29434  a12study  29754  isltrn2N  30931  cdlemefrs32fva  31211
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator