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  617  pm2.67-2  667  oibabs  834  pm2.85dc  845  peircedc  854  3jaob  1234  hbim  1478  hbimd  1506  i19.39  1572  hbae  1647  sbcof2  1732  sb4or  1755  tfi  4331  dmcosseq  4631  fliftfun  5467  tfrcl  6013  ac6sfi  6431  setindis  10920  bdsetindis  10922
  Copyright terms: Public domain W3C validator