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  690  imnan  692  pm4.53r  753  ioran  754  pm3.1  756  oranim  783  xornbi  1406  exalim  1526  exnalim  1670  festino  2161  calemes  2171  fresison  2173  calemos  2174  fesapo  2175  nner  2381  necon2ai  2431  necon2bi  2432  neneqad  2456  ralexim  2499  rexalim  2500  eueq3dc  2948  elndif  3298  ssddif  3408  unssdif  3409  n0i  3467  preleq  4607  dcextest  4633  dmsn0el  5157  funtpg  5330  ftpg  5775  acexmidlemab  5945  reldmtpos  6346  nntri2  6587  nntri3  6590  nndceq  6592  inffiexmid  7010  ctssdccl  7220  mkvprop  7267  elni2  7434  renfdisj  8139  sup3exmid  9037  fzdisj  10181  sumrbdclem  11732  prodrbdclem  11926  lgsval2lem  15531