Metamath Proof Explorer


Theorem dalemddea

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

Ref Expression
Hypothesis da.ps0 ( 𝜓 ↔ ( ( 𝑐𝐴𝑑𝐴 ) ∧ ¬ 𝑐 𝑌 ∧ ( 𝑑𝑐 ∧ ¬ 𝑑 𝑌𝐶 ( 𝑐 𝑑 ) ) ) )
Assertion dalemddea ( 𝜓𝑑𝐴 )

Proof

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