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  690  imnan  692  pm4.53r  753  ioran  754  pm3.1  756  oranim  783  xornbi  1406  exalim  1526  exnalim  1670  festino  2162  calemes  2172  fresison  2174  calemos  2175  fesapo  2176  nner  2382  necon2ai  2432  necon2bi  2433  neneqad  2457  ralexim  2500  rexalim  2501  eueq3dc  2954  elndif  3305  ssddif  3415  unssdif  3416  n0i  3474  preleq  4621  dcextest  4647  dmsn0el  5171  funtpg  5344  ftpg  5791  acexmidlemab  5961  reldmtpos  6362  nntri2  6603  nntri3  6606  nndceq  6608  inffiexmid  7029  ctssdccl  7239  mkvprop  7286  elni2  7462  renfdisj  8167  sup3exmid  9065  fzdisj  10209  sumrbdclem  11803  prodrbdclem  11997  lgsval2lem  15602