Theorem con2i 599

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 598	1 ⊢ (𝜓 → ¬ 𝜑)

Syntax hints:  ¬ wn 3   → wi 4

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-in1 586  ax-in2 587

This theorem is referenced by:  nsyl  600  notnot  601  imanim  660  imnan  662  pm4.53r  723  ioran  724  pm3.1  726  oranim  753  xornbi  1345  exalim  1459  exnalim  1606  festino  2079  calemes  2089  fresison  2091  calemos  2092  fesapo  2093  nner  2284  necon2ai  2334  necon2bi  2335  neneqad  2359  ralexim  2401  rexalim  2402  eueq3dc  2825  elndif  3164  ssddif  3274  unssdif  3275  n0i  3332  preleq  4428  dcextest  4453  dmsn0el  4964  funtpg  5130  ftpg  5556  acexmidlemab  5720  reldmtpos  6102  nntri2  6342  nntri3  6345  nndceq  6347  inffiexmid  6751  ctssdccl  6946  mkvprop  6979  elni2  7064  renfdisj  7742  sup3exmid  8619  fzdisj  9719  sumrbdclem  11031