ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  imim1i GIF version

Theorem imim1i 58
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 57 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  95  bi3ant  217  pm3.41  318  pm3.42  319  jarl  594  pm2.67-2  644  oibabs  811  pm2.85dc  822  peircedc  831  3jaob  1208  hbim  1453  hbimd  1481  i19.39  1547  hbae  1622  sbcof2  1707  sb4or  1730  tfi  4333  dmcosseq  4631  fliftfun  5464  ac6sfi  6383  setindis  10479  bdsetindis  10481
  Copyright terms: Public domain W3C validator