Theorem con2i 632

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

Syntax hints:  ¬ wn 3   → wi 4

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

This theorem is referenced by:  nsyl  633  notnot  634  imanim  695  imnan  697  pm4.53r  759  ioran  760  pm3.1  762  oranim  789  xornbi  1431  exalim  1551  exnalim  1695  festino  2187  calemes  2197  fresison  2199  calemos  2200  fesapo  2201  nner  2416  necon2ai  2466  necon2bi  2467  neneqad  2491  ralexim  2534  rexalim  2535  eueq3dc  2990  elndif  3342  ssddif  3454  unssdif  3455  n0i  3513  preleq  4676  dcextest  4702  dmsn0el  5231  funtpg  5406  ftpg  5867  acexmidlemab  6043  reldmtpos  6483  nntri2  6726  nntri3  6729  nndceq  6731  inffiexmid  7165  ctssdccl  7401  mkvprop  7448  elni2  7625  renfdisj  8329  sup3exmid  9227  fzdisj  10382  sumrbdclem  12056  prodrbdclem  12250  lgsval2lem  15870  g0wlk0  16352  clwwlknnn  16394