Theorem con2i 616

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 615	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 603  ax-in2 604

This theorem is referenced by:  nsyl  617  notnot  618  imanim  677  imnan  679  pm4.53r  740  ioran  741  pm3.1  743  oranim  770  xornbi  1364  exalim  1478  exnalim  1625  festino  2105  calemes  2115  fresison  2117  calemos  2118  fesapo  2119  nner  2312  necon2ai  2362  necon2bi  2363  neneqad  2387  ralexim  2429  rexalim  2430  eueq3dc  2858  elndif  3200  ssddif  3310  unssdif  3311  n0i  3368  preleq  4470  dcextest  4495  dmsn0el  5008  funtpg  5174  ftpg  5604  acexmidlemab  5768  reldmtpos  6150  nntri2  6390  nntri3  6393  nndceq  6395  inffiexmid  6800  ctssdccl  6996  mkvprop  7032  elni2  7122  renfdisj  7824  sup3exmid  8715  fzdisj  9832  sumrbdclem  11146  prodrbdclem  11340