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  1365  exalim  1479  exnalim  1626  festino  2106  calemes  2116  fresison  2118  calemos  2119  fesapo  2120  nner  2313  necon2ai  2363  necon2bi  2364  neneqad  2388  ralexim  2430  rexalim  2431  eueq3dc  2862  elndif  3205  ssddif  3315  unssdif  3316  n0i  3373  preleq  4478  dcextest  4503  dmsn0el  5016  funtpg  5182  ftpg  5612  acexmidlemab  5776  reldmtpos  6158  nntri2  6398  nntri3  6401  nndceq  6403  inffiexmid  6808  ctssdccl  7004  mkvprop  7040  elni2  7146  renfdisj  7848  sup3exmid  8739  fzdisj  9863  sumrbdclem  11178  prodrbdclem  11372