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	|- ( 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 627	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 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  2935  elndif  3284  ssddif  3394  unssdif  3395  n0i  3453  preleq  4588  dcextest  4614  dmsn0el  5136  funtpg  5306  ftpg  5743  acexmidlemab  5913  reldmtpos  6308  nntri2  6549  nntri3  6552  nndceq  6554  inffiexmid  6964  ctssdccl  7172  mkvprop  7219  elni2  7376  renfdisj  8081  sup3exmid  8978  fzdisj  10121  sumrbdclem  11523  prodrbdclem  11717  lgsval2lem  15167