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  2556  necon2bi  2562  necon4ai  2575  neneqad  2586  eueq3  3011  ssnpss  3372  psstr  3373  elndif  3390  n0i  3555  dfphi2  4569  phi011lem1  4598