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

Metamath Proof Explorer

Theorem cdleme31sc

Description: Part of proof of Lemma E in Crawley p. 113. (Contributed by NM, 31-Mar-2013)

		Ref	Expression
	Hypotheses	cdleme31sc.c	$⊢ C = (s \underset{˙}{\lor} U) \underset{˙}{\land} (Q \underset{˙}{\lor} ((P \underset{˙}{\lor} s) \underset{˙}{\land} W))$
		cdleme31sc.x	$⊢ X = (R \underset{˙}{\lor} U) \underset{˙}{\land} (Q \underset{˙}{\lor} ((P \underset{˙}{\lor} R) \underset{˙}{\land} W))$
	Assertion	cdleme31sc	$⊢ R \in A \to ⦋ R / s ⦌ C = X$

Proof

Step	Hyp	Ref	Expression
1		cdleme31sc.c	$⊢ C = (s \underset{˙}{\lor} U) \underset{˙}{\land} (Q \underset{˙}{\lor} ((P \underset{˙}{\lor} s) \underset{˙}{\land} W))$
2		cdleme31sc.x	$⊢ X = (R \underset{˙}{\lor} U) \underset{˙}{\land} (Q \underset{˙}{\lor} ((P \underset{˙}{\lor} R) \underset{˙}{\land} W))$
3		nfcvd	$⊢ R \in A \to \underline{Ⅎ} s ((R \underset{˙}{\lor} U) \underset{˙}{\land} (Q \underset{˙}{\lor} ((P \underset{˙}{\lor} R) \underset{˙}{\land} W)))$
4		oveq1	$⊢ s = R \to s \underset{˙}{\lor} U = R \underset{˙}{\lor} U$
5		oveq2	$⊢ s = R \to P \underset{˙}{\lor} s = P \underset{˙}{\lor} R$
6	5	oveq1d	$⊢ s = R \to (P \underset{˙}{\lor} s) \underset{˙}{\land} W = (P \underset{˙}{\lor} R) \underset{˙}{\land} W$
7	6	oveq2d	$⊢ s = R \to Q \underset{˙}{\lor} ((P \underset{˙}{\lor} s) \underset{˙}{\land} W) = Q \underset{˙}{\lor} ((P \underset{˙}{\lor} R) \underset{˙}{\land} W)$
8	4 7	oveq12d	$⊢ s = R \to (s \underset{˙}{\lor} U) \underset{˙}{\land} (Q \underset{˙}{\lor} ((P \underset{˙}{\lor} s) \underset{˙}{\land} W)) = (R \underset{˙}{\lor} U) \underset{˙}{\land} (Q \underset{˙}{\lor} ((P \underset{˙}{\lor} R) \underset{˙}{\land} W))$
9	3 8	csbiegf	$⊢ R \in A \to ⦋ R / s ⦌ ((s \underset{˙}{\lor} U) \underset{˙}{\land} (Q \underset{˙}{\lor} ((P \underset{˙}{\lor} s) \underset{˙}{\land} W))) = (R \underset{˙}{\lor} U) \underset{˙}{\land} (Q \underset{˙}{\lor} ((P \underset{˙}{\lor} R) \underset{˙}{\land} W))$
10	1	csbeq2i	$⊢ ⦋ R / s ⦌ C = ⦋ R / s ⦌ ((s \underset{˙}{\lor} U) \underset{˙}{\land} (Q \underset{˙}{\lor} ((P \underset{˙}{\lor} s) \underset{˙}{\land} W)))$
11	9 10 2	3eqtr4g	$⊢ R \in A \to ⦋ R / s ⦌ C = X$