Theorem con2i 630

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

Syntax hints:  ¬ wn 3   → wi 4

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

This theorem is referenced by:  nsyl  631  notnot  632  imanim  692  imnan  694  pm4.53r  756  ioran  757  pm3.1  759  oranim  786  xornbi  1428  exalim  1548  exnalim  1692  festino  2184  calemes  2194  fresison  2196  calemos  2197  fesapo  2198  nner  2404  necon2ai  2454  necon2bi  2455  neneqad  2479  ralexim  2522  rexalim  2523  eueq3dc  2977  elndif  3328  ssddif  3438  unssdif  3439  n0i  3497  preleq  4648  dcextest  4674  dmsn0el  5201  funtpg  5375  ftpg  5830  acexmidlemab  6004  reldmtpos  6410  nntri2  6653  nntri3  6656  nndceq  6658  inffiexmid  7084  ctssdccl  7294  mkvprop  7341  elni2  7517  renfdisj  8222  sup3exmid  9120  fzdisj  10265  sumrbdclem  11909  prodrbdclem  12103  lgsval2lem  15710  g0wlk0  16142  clwwlknnn  16181