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

Theorem con2i 590
 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 589 1 (𝜓 → ¬ 𝜑)
 Colors of variables: wff set class Syntax hints:  ¬ wn 3   → wi 4 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-in1 577  ax-in2 578 This theorem is referenced by:  nsyl  591  notnot  592  imnan  657  ioran  702  pm3.1  704  imanim  819  pm4.53r  838  oranim  841  xornbi  1318  exalim  1432  exnalim  1578  festino  2049  calemes  2059  fresison  2061  calemos  2062  fesapo  2063  nner  2253  necon2ai  2303  necon2bi  2304  neneqad  2328  ralexim  2365  rexalim  2366  eueq3dc  2775  elndif  3106  ssddif  3214  unssdif  3215  n0i  3272  preleq  4326  dmsn0el  4840  funtpg  5001  ftpg  5400  acexmidlemab  5558  reldmtpos  5923  nntri2  6159  nntri3  6162  nndceq  6164  inffiexmid  6458  elni2  6636  renfdisj  7309  fzdisj  9217  isumrblem  10418
 Copyright terms: Public domain W3C validator