Theorem con2i 636

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 635	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 623  ax-in2 624

This theorem is referenced by:  nsyl  637  notnot  638  imanim  699  imnan  701  pm4.53r  763  ioran  764  pm3.1  766  oranim  793  xornbi  1435  exalim  1555  exnalim  1699  festino  2193  calemes  2203  fresison  2205  calemos  2206  fesapo  2207  nner  2424  necon2ai  2474  necon2bi  2475  neneqad  2499  ralexim  2542  rexalim  2543  eueq3dc  3000  elndif  3353  ssddif  3465  unssdif  3466  n0i  3527  preleq  4697  dcextest  4723  dmsn0el  5252  funtpg  5427  ftpg  5890  acexmidlemab  6069  reldmtpos  6514  nntri2  6757  nntri3  6760  nndceq  6762  inffiexmid  7203  ctssdccl  7441  mkvprop  7488  elni2  7671  renfdisj  8375  sup3exmid  9277  fzdisj  10435  sumrbdclem  12122  prodrbdclem  12316  lgsval2lem  16043  g0wlk0  16525  clwwlknnn  16567