Metamath Proof Explorer


Theorem dalem-ccly

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

Ref Expression
Hypothesis da.ps0 ψ c A d A ¬ c ˙ Y d c ¬ d ˙ Y C ˙ c ˙ d
Assertion dalem-ccly ψ ¬ c ˙ Y

Proof

Step Hyp Ref Expression
1 da.ps0 ψ c A d A ¬ c ˙ Y d c ¬ d ˙ Y C ˙ c ˙ d
2 1 simp2bi ψ ¬ c ˙ Y