Theorem con2i 589

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

Syntax hints:  ¬ wn 3   → wi 4

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

This theorem is referenced by:  nsyl  590  notnot  591  imnan  656  ioran  701  pm3.1  703  imanim  818  pm4.53r  837  oranim  840  xornbi  1317  exalim  1431  exnalim  1577  festino  2047  calemes  2057  fresison  2059  calemos  2060  fesapo  2061  nner  2249  necon2ai  2299  necon2bi  2300  neneqad  2324  ralexim  2360  rexalim  2361  eueq3dc  2766  elndif  3096  ssddif  3198  unssdif  3199  n0i  3256  preleq  4298  dmsn0el  4810  funtpg  4970  ftpg  5368  acexmidlemab  5526  reldmtpos  5891  nntri2  6096  nntri3  6098  nndceq  6100  elni2  6504  renfdisj  7172  fzdisj  9071