Theorem con2i 557

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 556	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 544  ax-in2 545

This theorem is referenced by:  nsyl  558  notnot  559  imnan  624  ioran  669  pm3.1  671  imanim  785  pm4.53r  804  oranim  807  xornbi  1277  exalim  1391  exnalim  1537  festino  2006  calemes  2016  fresison  2018  calemos  2019  fesapo  2020  nner  2210  necon2ai  2259  necon2bi  2260  neneqad  2284  ralexim  2318  rexalim  2319  eueq3dc  2715  ssnpss  3047  psstr  3049  sspsstr  3050  psssstr  3051  elndif  3068  ssddif  3171  unssdif  3172  n0i  3229  disj4im  3276  preleq  4279  dmsn0el  4790  funtpg  4950  ftpg  5347  acexmidlemab  5506  reldmtpos  5868  nntri2  6073  nntri3  6075  nndceq  6077  elni2  6412  renfdisj  7079  fzdisj  8916