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  223  pm3.41  327  pm3.42  328  jarl  630  pm2.67-2  685  oibabs  686  stdcn  815  pm2.85dc  873  peircedc  882  3jaob  1263  hbim  1507  hbimd  1535  i19.39  1602  hbae  1679  sbcof2  1764  sb4or  1787  tfi  4464  dmcosseq  4778  fliftfun  5663  tfrcl  6227  ac6sfi  6758  fsum2d  11144  fsumabs  11174  fsumiun  11186  bj-nnsn  12747  bj-pm2.18st  12760  setindis  12967  bdsetindis  12969
  Copyright terms: Public domain W3C validator