Theorem necon3d 1607

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 1605	. 2 |- (ph -> (C =/= D -> -. A = B))
3		df-ne 1590	. 2 |- (A =/= B <-> -. A = B)
4	2, 3	syl6ibr 213	1 |- (ph -> (C =/= D -> A =/= B))

Syntax hints:  -. wn 2   -> wi 3   = wceq 958   =/= wne 1588

This theorem is referenced by:  necon3i 1608  ssne0 2309  pssdifn0 2333  omord 4205  kmlem9 4783  fseqsupcl 6526  fseqsupub 6527  geoisumr 7243  infxpidmlem10 7562  0ntr 7699  elcls3 7708  neindisj 7728  bcthlem10 8005  nmlno0lem 8449  hlipgt0 8612  h1dn0 9470  spansneleq 9488  h1datom 9499  nmlnop0ALT 9915  superpos 10276  irred 10316

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 1590

Copyright terms: Public domain