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  2790  elndif  3125  ssddif  3234  unssdif  3235  n0i  3292  preleq  4384  dcextest  4409  dmsn0el  4913  funtpg  5078  ftpg  5495  acexmidlemab  5660  reldmtpos  6032  nntri2  6269  nntri3  6272  nndceq  6274  inffiexmid  6676  elni2  6934  renfdisj  7607  fzdisj  9527  isumrblem  10826