New Foundations Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  NFE Home  >  Th. List  >  con2i GIF version

Theorem con2i 112
 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 111 1 (ψ → ¬ φ)
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8 This theorem is referenced by:  nsyl  113  notnot1  114  pm2.65i  165  pm3.14  488  pclem6  896  19.8wOLD  1693  hba1w  1707  ax5o  1749  19.8a  1756  hba1OLD  1787  spimehOLD  1821  ax12olem3  1929  spime  1976  sbn  2062  spsbe  2075  hba1-o  2149  festino  2309  calemes  2319  fresison  2321  calemos  2322  fesapo  2323  necon3ai  2556  necon2bi  2562  necon4ai  2575  neneqad  2586  eueq3  3011  ssnpss  3372  psstr  3373  elndif  3390  n0i  3555  dfphi2  4569  phi011lem1  4598
 Copyright terms: Public domain W3C validator