Theorem con2i 628

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

Syntax hints:  ¬ wn 3   → wi 4

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

This theorem is referenced by:  nsyl  629  notnot  630  imanim  689  imnan  691  pm4.53r  752  ioran  753  pm3.1  755  oranim  782  xornbi  1397  exalim  1516  exnalim  1660  festino  2151  calemes  2161  fresison  2163  calemos  2164  fesapo  2165  nner  2371  necon2ai  2421  necon2bi  2422  neneqad  2446  ralexim  2489  rexalim  2490  eueq3dc  2938  elndif  3287  ssddif  3397  unssdif  3398  n0i  3456  preleq  4591  dcextest  4617  dmsn0el  5139  funtpg  5309  ftpg  5746  acexmidlemab  5916  reldmtpos  6311  nntri2  6552  nntri3  6555  nndceq  6557  inffiexmid  6967  ctssdccl  7177  mkvprop  7224  elni2  7381  renfdisj  8086  sup3exmid  8984  fzdisj  10127  sumrbdclem  11542  prodrbdclem  11736  lgsval2lem  15251