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  694  imnan  696  pm4.53r  758  ioran  759  pm3.1  761  oranim  788  xornbi  1430  exalim  1550  exnalim  1694  festino  2185  calemes  2195  fresison  2197  calemos  2198  fesapo  2199  nner  2405  necon2ai  2455  necon2bi  2456  neneqad  2480  ralexim  2523  rexalim  2524  eueq3dc  2979  elndif  3330  ssddif  3440  unssdif  3441  n0i  3499  preleq  4655  dcextest  4681  dmsn0el  5208  funtpg  5383  ftpg  5841  acexmidlemab  6017  reldmtpos  6424  nntri2  6667  nntri3  6670  nndceq  6672  inffiexmid  7103  ctssdccl  7315  mkvprop  7362  elni2  7539  renfdisj  8244  sup3exmid  9142  fzdisj  10292  sumrbdclem  11961  prodrbdclem  12155  lgsval2lem  15768  g0wlk0  16250  clwwlknnn  16292