Theorem dalemccnedd

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

	Ref	Expression
Hypothesis	da.ps0	⊢ ( 𝜓 ↔ ( ( 𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐴 ) ∧ ¬ 𝑐 ≤ 𝑌 ∧ ( 𝑑 ≠ 𝑐 ∧ ¬ 𝑑 ≤ 𝑌 ∧ 𝐶 ≤ ( 𝑐 ∨ 𝑑 ) ) ) )
Assertion	dalemccnedd	⊢ ( 𝜓 → 𝑐 ≠ 𝑑 )

Proof

Step	Hyp	Ref	Expression
1		da.ps0	⊢ ( 𝜓 ↔ ( ( 𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐴 ) ∧ ¬ 𝑐 ≤ 𝑌 ∧ ( 𝑑 ≠ 𝑐 ∧ ¬ 𝑑 ≤ 𝑌 ∧ 𝐶 ≤ ( 𝑐 ∨ 𝑑 ) ) ) )
2		simp31	⊢ ( ( ( 𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐴 ) ∧ ¬ 𝑐 ≤ 𝑌 ∧ ( 𝑑 ≠ 𝑐 ∧ ¬ 𝑑 ≤ 𝑌 ∧ 𝐶 ≤ ( 𝑐 ∨ 𝑑 ) ) ) → 𝑑 ≠ 𝑐 )
3	1 2	sylbi	⊢ ( 𝜓 → 𝑑 ≠ 𝑐 )
4	3	necomd	⊢ ( 𝜓 → 𝑐 ≠ 𝑑 )