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

Metamath Proof Explorer

Theorem cdleme31se

Description: Part of proof of Lemma D in Crawley p. 113. (Contributed by NM, 26-Feb-2013)

		Ref	Expression
	Hypotheses	cdleme31se.e	$⊢ E = (P \underset{˙}{\lor} Q) \underset{˙}{\land} (D \underset{˙}{\lor} ((s \underset{˙}{\lor} T) \underset{˙}{\land} W))$
		cdleme31se.y	$⊢ Y = (P \underset{˙}{\lor} Q) \underset{˙}{\land} (D \underset{˙}{\lor} ((R \underset{˙}{\lor} T) \underset{˙}{\land} W))$
	Assertion	cdleme31se	$⊢ R \in A \to ⦋ R / s ⦌ E = Y$

Proof

Step	Hyp	Ref	Expression
1		cdleme31se.e	$⊢ E = (P \underset{˙}{\lor} Q) \underset{˙}{\land} (D \underset{˙}{\lor} ((s \underset{˙}{\lor} T) \underset{˙}{\land} W))$
2		cdleme31se.y	$⊢ Y = (P \underset{˙}{\lor} Q) \underset{˙}{\land} (D \underset{˙}{\lor} ((R \underset{˙}{\lor} T) \underset{˙}{\land} W))$
3		nfcvd	$⊢ R \in A \to \underline{Ⅎ} s ((P \underset{˙}{\lor} Q) \underset{˙}{\land} (D \underset{˙}{\lor} ((R \underset{˙}{\lor} T) \underset{˙}{\land} W)))$
4		oveq1	$⊢ s = R \to s \underset{˙}{\lor} T = R \underset{˙}{\lor} T$
5	4	oveq1d	$⊢ s = R \to (s \underset{˙}{\lor} T) \underset{˙}{\land} W = (R \underset{˙}{\lor} T) \underset{˙}{\land} W$
6	5	oveq2d	$⊢ s = R \to D \underset{˙}{\lor} ((s \underset{˙}{\lor} T) \underset{˙}{\land} W) = D \underset{˙}{\lor} ((R \underset{˙}{\lor} T) \underset{˙}{\land} W)$
7	6	oveq2d	$⊢ s = R \to (P \underset{˙}{\lor} Q) \underset{˙}{\land} (D \underset{˙}{\lor} ((s \underset{˙}{\lor} T) \underset{˙}{\land} W)) = (P \underset{˙}{\lor} Q) \underset{˙}{\land} (D \underset{˙}{\lor} ((R \underset{˙}{\lor} T) \underset{˙}{\land} W))$
8	3 7	csbiegf	$⊢ R \in A \to ⦋ R / s ⦌ ((P \underset{˙}{\lor} Q) \underset{˙}{\land} (D \underset{˙}{\lor} ((s \underset{˙}{\lor} T) \underset{˙}{\land} W))) = (P \underset{˙}{\lor} Q) \underset{˙}{\land} (D \underset{˙}{\lor} ((R \underset{˙}{\lor} T) \underset{˙}{\land} W))$
9	1	csbeq2i	$⊢ ⦋ R / s ⦌ E = ⦋ R / s ⦌ ((P \underset{˙}{\lor} Q) \underset{˙}{\land} (D \underset{˙}{\lor} ((s \underset{˙}{\lor} T) \underset{˙}{\land} W)))$
10	8 9 2	3eqtr4g	$⊢ R \in A \to ⦋ R / s ⦌ E = Y$