dalemclccjdd

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

		Ref	Expression
	Hypothesis	da.ps0	$⊢ ψ \leftrightarrow ((c \in A \land d \in A) \land \neg c \underset{˙}{\leq} Y \land (d \neq c \land \neg d \underset{˙}{\leq} Y \land C \underset{˙}{\leq} (c \underset{˙}{\lor} d)))$
	Assertion	dalemclccjdd	$⊢ ψ \to C \underset{˙}{\leq} (c \underset{˙}{\lor} d)$

Step	Hyp	Ref	Expression
1		da.ps0	$⊢ ψ \leftrightarrow ((c \in A \land d \in A) \land \neg c \underset{˙}{\leq} Y \land (d \neq c \land \neg d \underset{˙}{\leq} Y \land C \underset{˙}{\leq} (c \underset{˙}{\lor} d)))$
2		simp33	$⊢ ((c \in A \land d \in A) \land \neg c \underset{˙}{\leq} Y \land (d \neq c \land \neg d \underset{˙}{\leq} Y \land C \underset{˙}{\leq} (c \underset{˙}{\lor} d))) \to C \underset{˙}{\leq} (c \underset{˙}{\lor} d)$
3	1 2	sylbi	$⊢ ψ \to C \underset{˙}{\leq} (c \underset{˙}{\lor} d)$

Metamath Proof Explorer