Theorem con3i 633

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 629	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 615  ax-in2 616

This theorem is referenced by:  notnotnot  635  conax1  654  pm5.21ni  704  pm2.45  739  pm2.46  740  pm3.14  754  3ianorr  1320  nalequcoms  1531  equidqe  1546  nnal  1663  ax6blem  1664  hbnt  1667  naecoms  1738  euor2  2103  moexexdc  2129  baroco  2152  necon3ai  2416  necon3bi  2417  nnral  2487  eueq3dc  2938  difin  3401  indifdir  3420  difrab  3438  csbprc  3497  ifandc  3600  nelpri  3647  nelprd  3649  opprc  3830  opprc1  3831  opprc2  3832  notnotsnex  4221  eldifpw  4513  nlimsucg  4603  nfvres  5593  nfunsn  5594  ressnop0  5744  ovprc  5958  ovprc1  5959  ovprc2  5960  mapprc  6712  ixpprc  6779  ixp0  6791  fiprc  6875  fidceq  6931  unfiexmid  6980  difinfsnlem  7166  3nsssucpw1  7305  onntri51  7309  onntri52  7313  fzdcel  10117  bcpasc  10860  flodddiv4lt  12105  bj-nnan  15392  bj-imnimnn  15394  nnnotnotr  15646  nninfsellemsuc  15666