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  695  imnan  697  pm4.53r  759  ioran  760  pm3.1  762  oranim  789  xornbi  1431  exalim  1551  exnalim  1695  festino  2189  calemes  2199  fresison  2201  calemos  2202  fesapo  2203  nner  2418  necon2ai  2468  necon2bi  2469  neneqad  2493  ralexim  2536  rexalim  2537  eueq3dc  2993  elndif  3345  ssddif  3457  unssdif  3458  n0i  3516  preleq  4679  dcextest  4705  dmsn0el  5234  funtpg  5409  ftpg  5870  acexmidlemab  6046  reldmtpos  6486  nntri2  6729  nntri3  6732  nndceq  6734  inffiexmid  7168  ctssdccl  7404  mkvprop  7451  elni2  7634  renfdisj  8338  sup3exmid  9236  fzdisj  10392  sumrbdclem  12071  prodrbdclem  12265  lgsval2lem  15932  g0wlk0  16414  clwwlknnn  16456