ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  imim1i 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  584  pm2.67-2  634  oibabs  800  pm2.85dc  811  peircedc  820  3jaob  1197  hbim  1437  hbimd  1465  i19.39  1531  hbae  1606  sbcof2  1691  sb4or  1714  tfi  4305  dmcosseq  4603  fliftfun  5436  ac6sfi  6352  setindis  10066  bdsetindis  10068
  Copyright terms: Public domain W3C validator