Theorem con2i 617

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

Syntax hints:  ¬ wn 3   → wi 4

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

This theorem is referenced by:  nsyl  618  notnot  619  imanim  678  imnan  680  pm4.53r  741  ioran  742  pm3.1  744  oranim  771  xornbi  1376  exalim  1490  exnalim  1634  festino  2120  calemes  2130  fresison  2132  calemos  2133  fesapo  2134  nner  2340  necon2ai  2390  necon2bi  2391  neneqad  2415  ralexim  2458  rexalim  2459  eueq3dc  2900  elndif  3246  ssddif  3356  unssdif  3357  n0i  3414  preleq  4532  dcextest  4558  dmsn0el  5073  funtpg  5239  ftpg  5669  acexmidlemab  5836  reldmtpos  6221  nntri2  6462  nntri3  6465  nndceq  6467  inffiexmid  6872  ctssdccl  7076  mkvprop  7122  elni2  7255  renfdisj  7958  sup3exmid  8852  fzdisj  9987  sumrbdclem  11318  prodrbdclem  11512  lgsval2lem  13551