dalem-ccly - Mathbox for Norm Megill

	Mathbox for Norm Megill		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > dalem-ccly		Structured version Visualization version GIF version

Theorem dalem-ccly 39269

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

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

**Assertion**
Ref	Expression
dalem-ccly	⊢ (𝜓 → ¬ 𝑐 ≤ 𝑌)

**Proof of Theorem dalem-ccly**
Step	Hyp	Ref	Expression
1		da.ps0	. 2 ⊢ (𝜓 ↔ ((𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐴) ∧ ¬ 𝑐 ≤ 𝑌 ∧ (𝑑 ≠ 𝑐 ∧ ¬ 𝑑 ≤ 𝑌 ∧ 𝐶 ≤ (𝑐 ∨ 𝑑))))
2	1	simp2bi 1143	1 ⊢ (𝜓 → ¬ 𝑐 ≤ 𝑌)

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 ∧ wa 394 ∧ w3a 1084 ∈ wcel 2098 ≠ wne 2929 class class class wbr 5149 (class class class)co 7418

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 206 df-an 395 df-3an 1086

This theorem is referenced by: dalemswapyzps 39274 dalemrotps 39275 dalem21 39278 dalem23 39280 dalem24 39281 dalem39 39295 dalem48 39304

	
		OSZAR »