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

Theorem imim1i 60
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 59 1 ((𝜓𝜒) → (𝜑𝜒))
Colors of variables: wff set class
Syntax hints:  wi 4
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7
This theorem is referenced by:  jarr  97  bi3ant  224  pm3.41  331  pm3.42  332  jarl  659  pm2.67-2  714  oibabs  715  stdcn  848  pm2.85dc  906  peircedc  915  3jaob  1313  hbim  1556  hbimd  1584  i19.39  1651  hbae  1729  sbcof2  1821  sb4or  1844  tfi  4599  dmcosseq  4916  fliftfun  5818  tfrcl  6389  ac6sfi  6926  fsum2d  11475  fsumabs  11505  fsumiun  11517  fprod2d  11663  bj-nnsn  14943  bj-pm2.18st  14960  setindis  15177  bdsetindis  15179
  Copyright terms: Public domain W3C validator