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 )

This proof depends on syntax axioms:   -. wn 3   -> wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-in1 623  ax-in2 624

This theorem is used 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  4702  dcextest  4728  dmsn0el  5257  funtpg  5432  ftpg  5899  acexmidlemab  6079  reldmtpos  6524  nntri2  6767  nntri3  6770  nndceq  6772  inffiexmid  7213  ctssdccl  7451  mkvprop  7498  elni2  7681  renfdisj  8385  sup3exmid  9287  fzdisj  10457  sumrbdclem  12144  prodrbdclem  12338  lgsval2lem  16129  g0wlk0  16611  clwwlknnn  16653