Theorem con2i 627

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 626	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 614  ax-in2 615

This theorem is referenced by:  nsyl  628  notnot  629  imanim  688  imnan  690  pm4.53r  751  ioran  752  pm3.1  754  oranim  781  xornbi  1386  exalim  1502  exnalim  1646  festino  2132  calemes  2142  fresison  2144  calemos  2145  fesapo  2146  nner  2351  necon2ai  2401  necon2bi  2402  neneqad  2426  ralexim  2469  rexalim  2470  eueq3dc  2911  elndif  3259  ssddif  3369  unssdif  3370  n0i  3428  preleq  4554  dcextest  4580  dmsn0el  5098  funtpg  5267  ftpg  5700  acexmidlemab  5868  reldmtpos  6253  nntri2  6494  nntri3  6497  nndceq  6499  inffiexmid  6905  ctssdccl  7109  mkvprop  7155  elni2  7312  renfdisj  8016  sup3exmid  8913  fzdisj  10051  sumrbdclem  11384  prodrbdclem  11578  lgsval2lem  14381