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

Theorem con2i 567
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 566 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 554  ax-in2 555
This theorem is referenced by:  nsyl  568  notnot  569  imnan  634  ioran  679  pm3.1  681  imanim  796  pm4.53r  815  oranim  818  xornbi  1293  exalim  1407  exnalim  1553  festino  2022  calemes  2032  fresison  2034  calemos  2035  fesapo  2036  nner  2224  necon2ai  2274  necon2bi  2275  neneqad  2299  ralexim  2335  rexalim  2336  eueq3dc  2737  ssnpss  3074  psstr  3076  sspsstr  3077  psssstr  3078  elndif  3095  ssddif  3198  unssdif  3199  n0i  3256  disj4im  3303  preleq  4306  dmsn0el  4817  funtpg  4977  ftpg  5374  acexmidlemab  5533  reldmtpos  5898  nntri2  6103  nntri3  6105  nndceq  6107  elni2  6469  renfdisj  7137  fzdisj  9017
  Copyright terms: Public domain W3C validator