Theorem dalemccnedd

Description: Lemma for dath . Frequently-used utility lemma. (Contributed by NM, 15-Aug-2012)

	Ref	Expression
Hypothesis	da.ps0	|- ( ps <-> ( ( c e. A /\ d e. A ) /\ -. c .<_ Y /\ ( d =/= c /\ -. d .<_ Y /\ C .<_ ( c .\/ d ) ) ) )
Assertion	dalemccnedd	|- ( ps -> c =/= d )

Proof

Step	Hyp	Ref	Expression
1		da.ps0	|- ( ps <-> ( ( c e. A /\ d e. A ) /\ -. c .<_ Y /\ ( d =/= c /\ -. d .<_ Y /\ C .<_ ( c .\/ d ) ) ) )
2		simp31	|- ( ( ( c e. A /\ d e. A ) /\ -. c .<_ Y /\ ( d =/= c /\ -. d .<_ Y /\ C .<_ ( c .\/ d ) ) ) -> d =/= c )
3	1 2	sylbi	|- ( ps -> d =/= c )
4	3	necomd	|- ( ps -> c =/= d )