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  2186  calemes  2196  fresison  2198  calemos  2199  fesapo  2200  nner  2407  necon2ai  2457  necon2bi  2458  neneqad  2482  ralexim  2525  rexalim  2526  eueq3dc  2981  elndif  3333  ssddif  3443  unssdif  3444  n0i  3502  preleq  4659  dcextest  4685  dmsn0el  5213  funtpg  5388  ftpg  5846  acexmidlemab  6022  reldmtpos  6462  nntri2  6705  nntri3  6708  nndceq  6710  inffiexmid  7141  ctssdccl  7353  mkvprop  7400  elni2  7577  renfdisj  8281  sup3exmid  9179  fzdisj  10332  sumrbdclem  12001  prodrbdclem  12195  lgsval2lem  15812  g0wlk0  16294  clwwlknnn  16336