Theorem con2i 628

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

Syntax hints:  ¬ wn 3   → wi 4

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

This theorem is referenced by:  nsyl  629  notnot  630  imanim  689  imnan  691  pm4.53r  752  ioran  753  pm3.1  755  oranim  782  xornbi  1397  exalim  1513  exnalim  1657  festino  2148  calemes  2158  fresison  2160  calemos  2161  fesapo  2162  nner  2368  necon2ai  2418  necon2bi  2419  neneqad  2443  ralexim  2486  rexalim  2487  eueq3dc  2934  elndif  3283  ssddif  3393  unssdif  3394  n0i  3452  preleq  4587  dcextest  4613  dmsn0el  5135  funtpg  5305  ftpg  5742  acexmidlemab  5912  reldmtpos  6306  nntri2  6547  nntri3  6550  nndceq  6552  inffiexmid  6962  ctssdccl  7170  mkvprop  7217  elni2  7374  renfdisj  8079  sup3exmid  8976  fzdisj  10118  sumrbdclem  11520  prodrbdclem  11714  lgsval2lem  15126