Theorem necon4d 2818

Description: Contrapositive inference for inequality. (Contributed by NM, 2-Apr-2007.) (Proof shortened by Andrew Salmon, 25-May-2011.)

Hypothesis

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

Assertion

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

Proof of Theorem necon4d

Step	Hyp	Ref	Expression
1		necon4d.1	. . 3 |- ( ph -> ( A =/= B -> C =/= D ) )
2	1	necon2bd 2810	. 2 |- ( ph -> ( C = D -> -. A =/= B ) )
3		nne 2798	. 2 |- ( -. A =/= B <-> A = B )
4	2, 3	syl6ib 241	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:  oa00  7639  map0g  7897  epfrs  8607  fin23lem24  9144  abs00  14029  oddvds  17966  isabvd  18820  01eq0ring  19272  uvcf1  20131  lindff1  20159  hausnei2  21157  dfconn2  21222  hausflimi  21784  hauspwpwf1  21791  cxpeq0  24424  his6  27956  nn0sqeq1  29513  lkreqN  34457  ltrnideq  35462  hdmapip0  37207  rpnnen3  37599