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=\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\wedge }\left(D\underset{\dot{}}{\vee }\left(\left(s\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\wedge }W\right)\right)$$
	cdleme31se.y	$$⊢Y=\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\wedge }\left(D\underset{\dot{}}{\vee }\left(\left(R\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\wedge }W\right)\right)$$
Assertion	cdleme31se	$$⊢R\in A\to ⦋R/s⦌E=Y$$

Proof

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