ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  con2i 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  notnot  559  imnan  624  ioran  669  pm3.1  671  imanim  785  pm4.53r  804  oranim  807  xornbi  1277  exalim  1391  exnalim  1537  festino  2006  calemes  2016  fresison  2018  calemos  2019  fesapo  2020  nner  2210  necon2ai  2256  necon2bi  2257  neneqad  2281  ralexim  2315  rexalim  2316  eueq3dc  2712  ssnpss  3044  psstr  3046  sspsstr  3047  psssstr  3048  elndif  3065  ssddif  3168  unssdif  3169  n0i  3226  disj4im  3273  preleq  4248  dmsn0el  4752  funtpg  4912  ftpg  5309  acexmidlemab  5468  reldmtpos  5830  nntri2  6035  nntri3  6037  nndceq  6039  elni2  6367  renfdisj  7033  fzdisj  8857
  Copyright terms: Public domain W3C validator