Theorem con3i 622

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 618	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 604  ax-in2 605

This theorem is referenced by:  notnotnot  624  conax1  643  pm5.21ni  693  pm2.45  728  pm2.46  729  pm3.14  743  3ianorr  1288  nalequcoms  1498  equidqe  1513  ax6blem  1629  hbnt  1632  naecoms  1703  euor2  2058  moexexdc  2084  baroco  2107  necon3ai  2358  necon3bi  2359  eueq3dc  2862  difin  3318  indifdir  3337  difrab  3355  csbprc  3413  ifandc  3513  nelpri  3556  nelprd  3558  opprc  3734  opprc1  3735  opprc2  3736  notnotsnex  4119  eldifpw  4406  nlimsucg  4489  nfvres  5462  nfunsn  5463  ressnop0  5609  ovprc  5814  ovprc1  5815  ovprc2  5816  mapprc  6554  ixpprc  6621  ixp0  6633  fiprc  6717  fidceq  6771  unfiexmid  6814  difinfsnlem  6992  fzdcel  9851  bcpasc  10544  flodddiv4lt  11669  bj-nnan  13119  bj-nnal  13120  bj-nnst  13135  nninfsellemsuc  13383