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  2912  elndif  3260  ssddif  3370  unssdif  3371  n0i  3429  preleq  4555  dcextest  4581  dmsn0el  5099  funtpg  5268  ftpg  5701  acexmidlemab  5869  reldmtpos  6254  nntri2  6495  nntri3  6498  nndceq  6500  inffiexmid  6906  ctssdccl  7110  mkvprop  7156  elni2  7313  renfdisj  8017  sup3exmid  8914  fzdisj  10052  sumrbdclem  11385  prodrbdclem  11579  lgsval2lem  14414