ILE Home 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  821  pm4.53r  840  oranim  843  xornbi  1320  exalim  1434  exnalim  1580  festino  2051  calemes  2061  fresison  2063  calemos  2064  fesapo  2065  nner  2255  necon2ai  2305  necon2bi  2306  neneqad  2330  ralexim  2368  rexalim  2369  eueq3dc  2780  elndif  3113  ssddif  3222  unssdif  3223  n0i  3280  preleq  4344  dcextest  4369  dmsn0el  4866  funtpg  5030  ftpg  5444  acexmidlemab  5607  reldmtpos  5972  nntri2  6209  nntri3  6212  nndceq  6214  inffiexmid  6574  elni2  6817  renfdisj  7490  fzdisj  9398  isumrblem  10655
  Copyright terms: Public domain W3C validator