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

Step	Hyp	Ref	Expression
1		con2i.a	. 2 ⊢ (φ → ¬ ψ)
2		id 19	. 2 ⊢ (ψ → ψ)
3	1, 2	nsyl3 111	1 ⊢ (ψ → ¬ φ)

Syntax hints:  ¬ wn 3   → wi 4

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 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  2557  necon2bi  2563  necon4ai  2576  neneqad  2587  eueq3  3012  ssnpss  3373  psstr  3374  elndif  3391  n0i  3556  dfphi2  4570  phi011lem1  4599