Theorem con2i 593

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 592	1 |- ( ps -> -. ph )

Syntax hints:   -. wn 3   -> wi 4

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-in1 580  ax-in2 581

This theorem is referenced by:  nsyl  594  notnot  595  imnan  660  ioran  705  pm3.1  707  imanim  824  pm4.53r  843  oranim  846  xornbi  1323  exalim  1437  exnalim  1583  festino  2055  calemes  2065  fresison  2067  calemos  2068  fesapo  2069  nner  2260  necon2ai  2310  necon2bi  2311  neneqad  2335  ralexim  2373  rexalim  2374  eueq3dc  2792  elndif  3127  ssddif  3236  unssdif  3237  n0i  3294  preleq  4386  dcextest  4411  dmsn0el  4915  funtpg  5080  ftpg  5497  acexmidlemab  5662  reldmtpos  6034  nntri2  6271  nntri3  6274  nndceq  6276  inffiexmid  6678  elni2  6936  renfdisj  7609  fzdisj  9529  isumrblem  10828