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  4552  dcextest  4578  dmsn0el  5095  funtpg  5264  ftpg  5697  acexmidlemab  5864  reldmtpos  6249  nntri2  6490  nntri3  6493  nndceq  6495  inffiexmid  6901  ctssdccl  7105  mkvprop  7151  elni2  7308  renfdisj  8011  sup3exmid  8908  fzdisj  10045  sumrbdclem  11376  prodrbdclem  11570  lgsval2lem  14193