ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  imim1i Unicode version

Theorem imim1i 60
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 59 1  |-  ( ( ps  ->  ch )  ->  ( ph  ->  ch ) )
Colors of variables: wff set 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  97  bi3ant  224  pm3.41  331  pm3.42  332  jarl  658  pm2.67-2  713  oibabs  714  stdcn  847  pm2.85dc  905  peircedc  914  3jaob  1302  hbim  1545  hbimd  1573  i19.39  1640  hbae  1718  sbcof2  1810  sb4or  1833  tfi  4580  dmcosseq  4897  fliftfun  5794  tfrcl  6362  ac6sfi  6895  fsum2d  11436  fsumabs  11466  fsumiun  11478  fprod2d  11624  bj-nnsn  14345  bj-pm2.18st  14362  setindis  14579  bdsetindis  14581
  Copyright terms: Public domain W3C validator