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  1525  exnalim  1669  festino  2160  calemes  2170  fresison  2172  calemos  2173  fesapo  2174  nner  2380  necon2ai  2430  necon2bi  2431  neneqad  2455  ralexim  2498  rexalim  2499  eueq3dc  2947  elndif  3297  ssddif  3407  unssdif  3408  n0i  3466  preleq  4603  dcextest  4629  dmsn0el  5152  funtpg  5325  ftpg  5768  acexmidlemab  5938  reldmtpos  6339  nntri2  6580  nntri3  6583  nndceq  6585  inffiexmid  7003  ctssdccl  7213  mkvprop  7260  elni2  7427  renfdisj  8132  sup3exmid  9030  fzdisj  10174  sumrbdclem  11688  prodrbdclem  11882  lgsval2lem  15487