Theorem necon1d 2816

Description: Contrapositive law deduction for inequality. (Contributed by NM, 28-Dec-2008.) (Proof shortened by Andrew Salmon, 25-May-2011.)

Hypothesis

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

Assertion

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

Proof of Theorem necon1d

Step	Hyp	Ref	Expression
1		necon1d.1	. . 3 |- ( ph -> ( A =/= B -> C = D ) )
2		nne 2798	. . 3 |- ( -. C =/= D <-> C = D )
3	1, 2	syl6ibr 242	. 2 |- ( ph -> ( A =/= B -> -. C =/= D ) )
4	3	necon4ad 2813	1 |- ( ph -> ( C =/= D -> A = B ) )

Syntax hints:   -. wn 3   -> wi 4   = wceq 1483   =/= wne 2794

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

This theorem depends on definitions:  df-bi 197  df-ne 2795

This theorem is referenced by:  disji  4637  mul02lem2  10213  xblss2ps  22206  xblss2  22207  lgsne0  25060  h1datomi  28440  eigorthi  28696  disjif  29391  lineintmo  32264  poimirlem6  33415  poimirlem7  33416  2llnmat  34810  2lnat  35070  tendospcanN  36312  dihmeetlem13N  36608  dochkrshp  36675