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  2994  elndif  3347  ssddif  3459  unssdif  3460  n0i  3518  preleq  4682  dcextest  4708  dmsn0el  5237  funtpg  5412  ftpg  5873  acexmidlemab  6052  reldmtpos  6497  nntri2  6740  nntri3  6743  nndceq  6745  inffiexmid  7179  ctssdccl  7415  mkvprop  7462  elni2  7645  renfdisj  8349  sup3exmid  9251  fzdisj  10409  sumrbdclem  12091  prodrbdclem  12285  lgsval2lem  16012  g0wlk0  16494  clwwlknnn  16536