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=\left(s\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }\left(\left(P\underset{\dot{}}{\vee }s\right)\underset{\dot{}}{\wedge }W\right)\right)$$
	cdleme31sc.x	$$⊢X=\left(R\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }\left(\left(P\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\wedge }W\right)\right)$$
Assertion	cdleme31sc	$$⊢R\in A\to ⦋R/s⦌C=X$$

Proof

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