Theorem necon3bid

Description: Deduction from equality to inequality. (Contributed by NM, 23-Feb-2005) (Proof shortened by Andrew Salmon, 25-May-2011)

	Ref	Expression
Hypothesis	necon3bid.1	|- ( ph -> ( A = B <-> C = D ) )
Assertion	necon3bid	|- ( ph -> ( A =/= B <-> C =/= D ) )

Proof

Step	Hyp	Ref	Expression
1		necon3bid.1	|- ( ph -> ( A = B <-> C = D ) )
2		df-ne	|- ( A =/= B <-> -. A = B )
3	1	necon3bbid	|- ( ph -> ( -. A = B <-> C =/= D ) )
4	2 3	bitrid	|- ( ph -> ( A =/= B <-> C =/= D ) )