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  2913  elndif  3261  ssddif  3371  unssdif  3372  n0i  3430  preleq  4556  dcextest  4582  dmsn0el  5100  funtpg  5269  ftpg  5703  acexmidlemab  5872  reldmtpos  6257  nntri2  6498  nntri3  6501  nndceq  6503  inffiexmid  6909  ctssdccl  7113  mkvprop  7159  elni2  7316  renfdisj  8020  sup3exmid  8917  fzdisj  10055  sumrbdclem  11388  prodrbdclem  11582  lgsval2lem  14551