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

Theorem con2i 616
 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 615 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 603  ax-in2 604 This theorem is referenced by:  nsyl  617  notnot  618  imanim  677  imnan  679  pm4.53r  740  ioran  741  pm3.1  743  oranim  770  xornbi  1364  exalim  1478  exnalim  1625  festino  2105  calemes  2115  fresison  2117  calemos  2118  fesapo  2119  nner  2312  necon2ai  2362  necon2bi  2363  neneqad  2387  ralexim  2429  rexalim  2430  eueq3dc  2858  elndif  3200  ssddif  3310  unssdif  3311  n0i  3368  preleq  4470  dcextest  4495  dmsn0el  5008  funtpg  5174  ftpg  5604  acexmidlemab  5768  reldmtpos  6150  nntri2  6390  nntri3  6393  nndceq  6395  inffiexmid  6800  ctssdccl  6996  mkvprop  7032  elni2  7122  renfdisj  7824  sup3exmid  8715  fzdisj  9832  sumrbdclem  11146  prodrbdclem  11340
 Copyright terms: Public domain W3C validator