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 ( 𝜓 ↔ ( ( 𝑐𝐴𝑑𝐴 ) ∧ ¬ 𝑐 𝑌 ∧ ( 𝑑𝑐 ∧ ¬ 𝑑 𝑌𝐶 ( 𝑐 𝑑 ) ) ) )
Assertion dalem-ccly ( 𝜓 → ¬ 𝑐 𝑌 )

Proof

Step Hyp Ref Expression
1 da.ps0 ( 𝜓 ↔ ( ( 𝑐𝐴𝑑𝐴 ) ∧ ¬ 𝑐 𝑌 ∧ ( 𝑑𝑐 ∧ ¬ 𝑑 𝑌𝐶 ( 𝑐 𝑑 ) ) ) )
2 1 simp2bi ( 𝜓 → ¬ 𝑐 𝑌 )