Theorem con2i 617

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	|- ( ph -> -. ps )

Assertion

Ref	Expression
con2i	|- ( ps -> -. ph )

Proof of Theorem con2i

Step	Hyp	Ref	Expression
1		con2i.a	. 2 |- ( ph -> -. ps )
2		id 19	. 2 |- ( ps -> ps )
3	1, 2	nsyl3 616	1 |- ( ps -> -. ph )

Syntax hints:   -. wn 3   -> wi 4

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

This theorem is referenced by:  nsyl  618  notnot  619  imanim  678  imnan  680  pm4.53r  741  ioran  742  pm3.1  744  oranim  771  xornbi  1368  exalim  1482  exnalim  1626  festino  2112  calemes  2122  fresison  2124  calemos  2125  fesapo  2126  nner  2331  necon2ai  2381  necon2bi  2382  neneqad  2406  ralexim  2449  rexalim  2450  eueq3dc  2886  elndif  3231  ssddif  3341  unssdif  3342  n0i  3399  preleq  4514  dcextest  4540  dmsn0el  5055  funtpg  5221  ftpg  5651  acexmidlemab  5818  reldmtpos  6200  nntri2  6441  nntri3  6444  nndceq  6446  inffiexmid  6851  ctssdccl  7055  mkvprop  7101  elni2  7234  renfdisj  7937  sup3exmid  8828  fzdisj  9954  sumrbdclem  11274  prodrbdclem  11468