Theorem con2i 632

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 631	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 619  ax-in2 620

This theorem is referenced by:  nsyl  633  notnot  634  imanim  695  imnan  697  pm4.53r  759  ioran  760  pm3.1  762  oranim  789  xornbi  1431  exalim  1551  exnalim  1695  festino  2187  calemes  2197  fresison  2199  calemos  2200  fesapo  2201  nner  2416  necon2ai  2466  necon2bi  2467  neneqad  2491  ralexim  2534  rexalim  2535  eueq3dc  2991  elndif  3343  ssddif  3455  unssdif  3456  n0i  3514  preleq  4677  dcextest  4703  dmsn0el  5232  funtpg  5407  ftpg  5868  acexmidlemab  6044  reldmtpos  6484  nntri2  6727  nntri3  6730  nndceq  6732  inffiexmid  7166  ctssdccl  7402  mkvprop  7449  elni2  7629  renfdisj  8333  sup3exmid  9231  fzdisj  10386  sumrbdclem  12063  prodrbdclem  12257  lgsval2lem  15883  g0wlk0  16365  clwwlknnn  16407