Theorem con2i 632

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

Syntax hints:  ¬ wn 3   → wi 4

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

This theorem is referenced by:  nsyl  633  notnot  634  imanim  694  imnan  696  pm4.53r  758  ioran  759  pm3.1  761  oranim  788  xornbi  1430  exalim  1550  exnalim  1694  festino  2186  calemes  2196  fresison  2198  calemos  2199  fesapo  2200  nner  2406  necon2ai  2456  necon2bi  2457  neneqad  2481  ralexim  2524  rexalim  2525  eueq3dc  2980  elndif  3331  ssddif  3441  unssdif  3442  n0i  3500  preleq  4653  dcextest  4679  dmsn0el  5206  funtpg  5381  ftpg  5838  acexmidlemab  6012  reldmtpos  6419  nntri2  6662  nntri3  6665  nndceq  6667  inffiexmid  7098  ctssdccl  7310  mkvprop  7357  elni2  7534  renfdisj  8239  sup3exmid  9137  fzdisj  10287  sumrbdclem  11940  prodrbdclem  12134  lgsval2lem  15742  g0wlk0  16224  clwwlknnn  16266