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  1405  exalim  1524  exnalim  1668  festino  2159  calemes  2169  fresison  2171  calemos  2172  fesapo  2173  nner  2379  necon2ai  2429  necon2bi  2430  neneqad  2454  ralexim  2497  rexalim  2498  eueq3dc  2946  elndif  3296  ssddif  3406  unssdif  3407  n0i  3465  preleq  4602  dcextest  4628  dmsn0el  5151  funtpg  5324  ftpg  5767  acexmidlemab  5937  reldmtpos  6338  nntri2  6579  nntri3  6582  nndceq  6584  inffiexmid  7002  ctssdccl  7212  mkvprop  7259  elni2  7426  renfdisj  8131  sup3exmid  9029  fzdisj  10173  sumrbdclem  11659  prodrbdclem  11853  lgsval2lem  15458