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

Theorem con2i 617
 Description: A contraposition inference. (Contributed by NM, 5-Aug-1993.) (Proof shortened by O'Cat, 28-Nov-2008.) (Proof shortened by Wolf Lammen, 13-Jun-2013.)
Hypothesis
Ref Expression
con2i.a (𝜑 → ¬ 𝜓)
Assertion
Ref Expression
con2i (𝜓 → ¬ 𝜑)

Proof of Theorem con2i
StepHypRef Expression
1 con2i.a . 2 (𝜑 → ¬ 𝜓)
2 id 19 . 2 (𝜓𝜓)
31, 2nsyl3 616 1 (𝜓 → ¬ 𝜑)
 Colors of variables: wff set class Syntax hints:  ¬ wn 3   → wi 4 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-in1 604  ax-in2 605 This theorem is referenced by:  nsyl  618  notnot  619  imanim  678  imnan  680  pm4.53r  741  ioran  742  pm3.1  744  oranim  771  xornbi  1365  exalim  1479  exnalim  1626  festino  2106  calemes  2116  fresison  2118  calemos  2119  fesapo  2120  nner  2313  necon2ai  2363  necon2bi  2364  neneqad  2388  ralexim  2431  rexalim  2432  eueq3dc  2863  elndif  3206  ssddif  3316  unssdif  3317  n0i  3374  preleq  4479  dcextest  4504  dmsn0el  5017  funtpg  5183  ftpg  5613  acexmidlemab  5777  reldmtpos  6159  nntri2  6399  nntri3  6402  nndceq  6404  inffiexmid  6809  ctssdccl  7006  mkvprop  7042  elni2  7166  renfdisj  7868  sup3exmid  8759  fzdisj  9883  sumrbdclem  11198  prodrbdclem  11392
 Copyright terms: Public domain W3C validator