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	|- ( 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 631	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 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  2186  calemes  2196  fresison  2198  calemos  2199  fesapo  2200  nner  2406  necon2ai  2456  necon2bi  2457  neneqad  2481  ralexim  2524  rexalim  2525  eueq3dc  2980  elndif  3331  ssddif  3441  unssdif  3442  n0i  3500  preleq  4653  dcextest  4679  dmsn0el  5206  funtpg  5381  ftpg  5837  acexmidlemab  6011  reldmtpos  6418  nntri2  6661  nntri3  6664  nndceq  6666  inffiexmid  7097  ctssdccl  7309  mkvprop  7356  elni2  7533  renfdisj  8238  sup3exmid  9136  fzdisj  10286  sumrbdclem  11937  prodrbdclem  12131  lgsval2lem  15738  g0wlk0  16220  clwwlknnn  16262