This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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	$⊢ ψ \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	dalem-ccly	$⊢ ψ \to \neg c \underset{˙}{\leq} Y$

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	1	simp2bi	$⊢ ψ \to \neg c \underset{˙}{\leq} Y$