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  568  pm2.67-2  618  oibabs  784  pm2.85dc  795  peircedc  804  3jaob  1178  hbim  1410  hbimd  1438  i19.39  1504  hbae  1579  sbcof2  1664  sb4or  1687  tfi  4220  dmcosseq  4518  fliftfun  5349  setindis  8347  bdsetindis  8349
  Copyright terms: Public domain W3C validator