Theorem con3i 561

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  580  pm5.21ni  618  notnotnot  627  pm2.45  656  pm2.46  657  pm3.14  669  3ianorr  1203  nalequcoms  1407  equidqe  1422  ax6blem  1537  hbnt  1540  naecoms  1609  euor2  1955  moexexdc  1981  baroco  2004  necon3ai  2248  necon3bi  2249  eueq3dc  2709  difin  3168  indifdir  3187  difrab  3205  csbprc  3256  nelpri  3388  opprc  3561  opprc1  3562  opprc2  3563  eldifpw  4174  nlimsucg  4242  nfvres  5149  nfunsn  5150  ressnop0  5287  ovprc  5482  ovprc1  5483  ovprc2  5484  fiprc  6228  fzdcel  8674