Theorem con3i 637

Description: A contraposition inference. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 20-Jun-2013.)

Hypothesis

Ref	Expression
con3i.a	|- ( ph -> ps )

Assertion

Ref	Expression
con3i	|- ( -. ps -> -. ph )

Proof of Theorem con3i

Step	Hyp	Ref	Expression
1		id 19	. 2 |- ( -. ps -> -. ps )
2		con3i.a	. 2 |- ( ph -> ps )
3	1, 2	nsyl 633	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 619  ax-in2 620

This theorem is referenced by:  notnotnot  639  nsyl5  655  conax1  659  pm5.21ni  711  pm2.45  746  pm2.46  747  pm3.14  761  3ianorr  1346  nalequcoms  1566  equidqe  1581  nnal  1698  hbn  1699  hbnt  1701  naecoms  1772  euor2  2138  moexexdc  2164  baroco  2187  necon3ai  2452  necon3bi  2453  nnral  2523  eueq3dc  2981  difin  3446  indifdir  3465  difrab  3483  csbprc  3542  ifandc  3650  nelpri  3697  nelprd  3699  opprc  3888  opprc1  3889  opprc2  3890  notnotsnex  4283  eldifpw  4580  nlimsucg  4670  nfvres  5684  nfunsn  5685  ressnop0  5843  ovprc  6064  ovprc1  6065  ovprc2  6066  mapprc  6864  ixpprc  6931  ixp0  6943  fiprc  7033  fidceq  7099  elssdc  7137  unfiexmid  7153  relprcnfsupp  7213  difinfsnlem  7358  3nsssucpw1  7514  onntri51  7518  onntri52  7522  fzdcel  10337  bcpasc  11091  pfxclz  11326  flodddiv4lt  12579  bj-nnan  16454  bj-imnimnn  16456  nnnotnotr  16706  nninfsellemsuc  16738