Theorem con2i 630

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

Syntax hints:  ¬ wn 3   → wi 4

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

This theorem is referenced by:  nsyl  631  notnot  632  imanim  692  imnan  694  pm4.53r  755  ioran  756  pm3.1  758  oranim  785  xornbi  1408  exalim  1528  exnalim  1672  festino  2164  calemes  2174  fresison  2176  calemos  2177  fesapo  2178  nner  2384  necon2ai  2434  necon2bi  2435  neneqad  2459  ralexim  2502  rexalim  2503  eueq3dc  2957  elndif  3308  ssddif  3418  unssdif  3419  n0i  3477  preleq  4624  dcextest  4650  dmsn0el  5174  funtpg  5348  ftpg  5796  acexmidlemab  5968  reldmtpos  6369  nntri2  6610  nntri3  6613  nndceq  6615  inffiexmid  7036  ctssdccl  7246  mkvprop  7293  elni2  7469  renfdisj  8174  sup3exmid  9072  fzdisj  10216  sumrbdclem  11854  prodrbdclem  12048  lgsval2lem  15654