Theorem con2i 636

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

Syntax hints:  ¬ wn 3   → wi 4

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

This theorem is referenced by:  nsyl  637  notnot  638  imanim  699  imnan  701  pm4.53r  763  ioran  764  pm3.1  766  oranim  793  xornbi  1435  exalim  1555  exnalim  1699  festino  2193  calemes  2203  fresison  2205  calemos  2206  fesapo  2207  nner  2424  necon2ai  2474  necon2bi  2475  neneqad  2499  ralexim  2542  rexalim  2543  eueq3dc  3000  elndif  3353  ssddif  3465  unssdif  3466  n0i  3527  preleq  4700  dcextest  4726  dmsn0el  5255  funtpg  5430  ftpg  5893  acexmidlemab  6073  reldmtpos  6518  nntri2  6761  nntri3  6764  nndceq  6766  inffiexmid  7207  ctssdccl  7445  mkvprop  7492  elni2  7675  renfdisj  8379  sup3exmid  9281  fzdisj  10440  sumrbdclem  12127  prodrbdclem  12321  lgsval2lem  16112  g0wlk0  16594  clwwlknnn  16636