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

Theorem con2i 557
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 556 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 544  ax-in2 545
This theorem is referenced by:  nsyl  558  notnot1  559  imnan  623  ioran  668  pm3.1  670  imanim  784  pm4.53r  803  oranim  806  xornbi  1274  exalim  1388  exnalim  1534  festino  2003  calemes  2013  fresison  2015  calemos  2016  fesapo  2017  nner  2207  necon2ai  2253  necon2bi  2254  neneqad  2278  ralexim  2312  rexalim  2313  eueq3dc  2709  ssnpss  3041  psstr  3043  sspsstr  3044  psssstr  3045  elndif  3062  ssddif  3165  unssdif  3166  n0i  3223  disj4im  3270  preleq  4233  dmsn0el  4733  funtpg  4893  ftpg  5290  acexmidlemab  5449  reldmtpos  5809  nntri2  6012  nntri3  6014  nndceq  6015  elni2  6298  renfdisj  6836  fzdisj  8646
  Copyright terms: Public domain W3C validator