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  1528  equidqe  1543  nnal  1660  ax6blem  1661  hbnt  1664  naecoms  1735  euor2  2100  moexexdc  2126  baroco  2149  necon3ai  2413  necon3bi  2414  nnral  2484  eueq3dc  2935  difin  3397  indifdir  3416  difrab  3434  csbprc  3493  ifandc  3596  nelpri  3643  nelprd  3645  opprc  3826  opprc1  3827  opprc2  3828  notnotsnex  4217  eldifpw  4509  nlimsucg  4599  nfvres  5589  nfunsn  5590  ressnop0  5740  ovprc  5954  ovprc1  5955  ovprc2  5956  mapprc  6708  ixpprc  6775  ixp0  6787  fiprc  6871  fidceq  6927  unfiexmid  6976  difinfsnlem  7160  3nsssucpw1  7298  onntri51  7302  onntri52  7306  fzdcel  10109  bcpasc  10840  flodddiv4lt  12080  bj-nnan  15298  bj-imnimnn  15300  nnnotnotr  15552  nninfsellemsuc  15572