Theorem necon3d 1596

Description: Contrapositive law deduction for inequality.

Hypothesis

Ref	Expression
necon3d.1	|- (ph -> (A = B -> C = D))

Assertion

Ref	Expression
necon3d	|- (ph -> (C =/= D -> A =/= B))

Proof of Theorem necon3d

Step	Hyp	Ref	Expression
1		necon3d.1	. . 3 |- (ph -> (A = B -> C = D))
2	1	necon3ad 1594	. 2 |- (ph -> (C =/= D -> -. A = B))
3		df-ne 1579	. 2 |- (A =/= B <-> -. A = B)
4	2, 3	syl6ibr 213	1 |- (ph -> (C =/= D -> A =/= B))

Syntax hints:  -. wn 2   -> wi 3   = wceq 953   =/= wne 1577

This theorem is referenced by:  necon3i 1597  ssne0 2295  pssdifn0 2319  omord 4183  kmlem9 4745  fseqsupcl 6457  fseqsupub 6458  geoisumr 7178  infxpidmlem10 7504  0ntr 7644  elcls3 7652  neindisj 7672  bcthlem10 7942  nmlno0lem 8385  hlipgt0 8546  h1dn0 9390  spansneleq 9409  h1datom 9421  nmlnop0ALT 9835  superpos 10189  irred 10229

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7

This theorem depends on definitions:  df-bi 147  df-ne 1579

Copyright terms: Public domain