Theorem con3i 562

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 558	1 |- ( -. ps -> -. ph )

Syntax hints:   -. wn 3   -> wi 4

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-in1 544  ax-in2 545

This theorem is referenced by:  pm2.51  581  pm5.21ni  619  notnotnot  628  pm2.45  657  pm2.46  658  pm3.14  670  3ianorr  1204  nalequcoms  1410  equidqe  1425  ax6blem  1540  hbnt  1543  naecoms  1612  euor2  1958  moexexdc  1984  baroco  2007  necon3ai  2254  necon3bi  2255  eueq3dc  2715  difin  3174  indifdir  3193  difrab  3211  csbprc  3262  nelpri  3399  opprc  3570  opprc1  3571  opprc2  3572  eldifpw  4208  nlimsucg  4290  nfvres  5206  nfunsn  5207  ressnop0  5344  ovprc  5540  ovprc1  5541  ovprc2  5542  fiprc  6292  fidceq  6330  fzdcel  8904