ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  imim1i Structured version   GIF 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 (φψ)
Assertion
Ref Expression
imim1i ((ψχ) → (φχ))

Proof of Theorem imim1i
StepHypRef Expression
1 imim1i.1 . 2 (φψ)
2 id 19 . 2 (χχ)
31, 2imim12i 53 1 ((ψχ) → (φχ))
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  91  bi3ant  213  pm3.41  314  pm3.42  315  jarl  583  pm2.67-2  633  oibabs  799  pm2.85dc  810  peircedc  819  3jaob  1196  hbim  1434  hbimd  1462  i19.39  1528  hbae  1603  sbcof2  1688  sb4or  1711  tfi  4248  dmcosseq  4546  fliftfun  5379  setindis  9427  bdsetindis  9429
  Copyright terms: Public domain W3C validator