| Mathbox for Norm Megill |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > Mathboxes > dalemccea | Structured version Visualization version GIF version | ||
| Description: Lemma for dath 39738. Frequently-used utility lemma. (Contributed by NM, 15-Aug-2012.) |
| Ref | Expression |
|---|---|
| da.ps0 | ⊢ (𝜓 ↔ ((𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐴) ∧ ¬ 𝑐 ≤ 𝑌 ∧ (𝑑 ≠ 𝑐 ∧ ¬ 𝑑 ≤ 𝑌 ∧ 𝐶 ≤ (𝑐 ∨ 𝑑)))) |
| Ref | Expression |
|---|---|
| dalemccea | ⊢ (𝜓 → 𝑐 ∈ 𝐴) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | da.ps0 | . 2 ⊢ (𝜓 ↔ ((𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐴) ∧ ¬ 𝑐 ≤ 𝑌 ∧ (𝑑 ≠ 𝑐 ∧ ¬ 𝑑 ≤ 𝑌 ∧ 𝐶 ≤ (𝑐 ∨ 𝑑)))) | |
| 2 | simp1l 1198 | . 2 ⊢ (((𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐴) ∧ ¬ 𝑐 ≤ 𝑌 ∧ (𝑑 ≠ 𝑐 ∧ ¬ 𝑑 ≤ 𝑌 ∧ 𝐶 ≤ (𝑐 ∨ 𝑑))) → 𝑐 ∈ 𝐴) | |
| 3 | 1, 2 | sylbi 217 | 1 ⊢ (𝜓 → 𝑐 ∈ 𝐴) |
| Colors of variables: wff setvar class |
| Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∧ wa 395 ∧ w3a 1087 ∈ wcel 2108 ≠ wne 2940 class class class wbr 5143 (class class class)co 7431 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-3an 1089 |
| This theorem is referenced by: dalemcceb 39691 dalemswapyzps 39692 dalemrotps 39693 dalemcjden 39694 dalem23 39698 dalem24 39699 dalem25 39700 dalem27 39701 dalem28 39702 dalem38 39712 dalem39 39713 dalem44 39718 dalem51 39725 dalem56 39730 |
| Copyright terms: Public domain | W3C validator |