Theorem con2i 622

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

Syntax hints:  ¬ wn 3   → wi 4

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

This theorem is referenced by:  nsyl  623  notnot  624  imanim  683  imnan  685  pm4.53r  746  ioran  747  pm3.1  749  oranim  776  xornbi  1381  exalim  1495  exnalim  1639  festino  2125  calemes  2135  fresison  2137  calemos  2138  fesapo  2139  nner  2344  necon2ai  2394  necon2bi  2395  neneqad  2419  ralexim  2462  rexalim  2463  eueq3dc  2904  elndif  3251  ssddif  3361  unssdif  3362  n0i  3420  preleq  4539  dcextest  4565  dmsn0el  5080  funtpg  5249  ftpg  5680  acexmidlemab  5847  reldmtpos  6232  nntri2  6473  nntri3  6476  nndceq  6478  inffiexmid  6884  ctssdccl  7088  mkvprop  7134  elni2  7276  renfdisj  7979  sup3exmid  8873  fzdisj  10008  sumrbdclem  11340  prodrbdclem  11534  lgsval2lem  13705