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

Theorem imim1i 59
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 58 1  |-  ( ( ps  ->  ch )  ->  ( ph  ->  ch ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7
This theorem is referenced by:  jarr  96  bi3ant  222  pm3.41  324  pm3.42  325  jarl  619  pm2.67-2  669  oibabs  838  pm2.85dc  849  peircedc  858  3jaob  1238  hbim  1482  hbimd  1510  i19.39  1576  hbae  1653  sbcof2  1738  sb4or  1761  tfi  4397  dmcosseq  4704  fliftfun  5575  tfrcl  6129  ac6sfi  6614  fsum2d  10829  fsumabs  10859  fsumiun  10871  setindis  11862  bdsetindis  11864
  Copyright terms: Public domain W3C validator