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  3288  ssddif  3398  unssdif  3399  n0i  3457  preleq  4592  dcextest  4618  dmsn0el  5140  funtpg  5310  ftpg  5749  acexmidlemab  5919  reldmtpos  6320  nntri2  6561  nntri3  6564  nndceq  6566  inffiexmid  6976  ctssdccl  7186  mkvprop  7233  elni2  7398  renfdisj  8103  sup3exmid  9001  fzdisj  10144  sumrbdclem  11559  prodrbdclem  11753  lgsval2lem  15335