Theorem con2i 590

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

Syntax hints:  ¬ wn 3   → wi 4

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

This theorem is referenced by:  nsyl  591  notnot  592  imnan  657  ioran  702  pm3.1  704  imanim  819  pm4.53r  838  oranim  841  xornbi  1318  exalim  1432  exnalim  1578  festino  2049  calemes  2059  fresison  2061  calemos  2062  fesapo  2063  nner  2253  necon2ai  2303  necon2bi  2304  neneqad  2328  ralexim  2365  rexalim  2366  eueq3dc  2775  elndif  3106  ssddif  3214  unssdif  3215  n0i  3272  preleq  4326  dmsn0el  4840  funtpg  5001  ftpg  5400  acexmidlemab  5558  reldmtpos  5923  nntri2  6159  nntri3  6162  nndceq  6164  inffiexmid  6458  elni2  6636  renfdisj  7309  fzdisj  9217  isumrblem  10418