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  223  pm3.41  329  pm3.42  330  jarl  648  pm2.67-2  703  oibabs  704  stdcn  837  pm2.85dc  895  peircedc  904  3jaob  1291  hbim  1532  hbimd  1560  i19.39  1627  hbae  1705  sbcof2  1797  sb4or  1820  tfi  4556  dmcosseq  4872  fliftfun  5761  tfrcl  6326  ac6sfi  6858  fsum2d  11370  fsumabs  11400  fsumiun  11412  fprod2d  11558  bj-nnsn  13508  bj-pm2.18st  13525  setindis  13742  bdsetindis  13744
  Copyright terms: Public domain W3C validator