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

Theorem con2i 545
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 544 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 532  ax-in2 533
This theorem is referenced by:  nsyl  546  notnot1  547  imnan  611  ioran  656  pm3.1  658  imanim  773  pm4.53r  792  oranim  795  xornbi  1258  exalim  1368  exnalim  1515  festino  1984  calemes  1994  fresison  1996  calemos  1997  fesapo  1998  nner  2188  necon2ai  2233  necon2bi  2234  neneqad  2258  ralexim  2292  rexalim  2293  eueq3dc  2688  ssnpss  3020  psstr  3022  sspsstr  3023  psssstr  3024  elndif  3041  ssddif  3144  unssdif  3145  n0i  3202  disj4im  3249  preleq  4213  dmsn0el  4713  funtpg  4872  ftpg  5268  acexmidlemab  5426  reldmtpos  5786  nntri2  5984  nndceq  5986  elni2  6168  renfdisj  6674
  Copyright terms: Public domain W3C validator