Theorem cdleme31se2

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

	Ref	Expression
Hypotheses	cdleme31se2.e	$$⊢E=\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)$$
	cdleme31se2.y	$$⊢Y=\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\wedge }\left(⦋S/t⦌D\underset{\dot{}}{\vee }\left(\left(R\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }W\right)\right)$$
Assertion	cdleme31se2	$$⊢S\in A\to ⦋S/t⦌E=Y$$

Proof

Step	Hyp	Ref	Expression
1		cdleme31se2.e	$$⊢E=\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)$$
2		cdleme31se2.y	$$⊢Y=\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\wedge }\left(⦋S/t⦌D\underset{\dot{}}{\vee }\left(\left(R\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }W\right)\right)$$
3		nfcv	$$⊢\underset{\_}{Ⅎ}t\left(P\underset{\dot{}}{\vee }Q\right)$$
4		nfcv	$$⊢\underset{\_}{Ⅎ}t\underset{\dot{}}{\wedge }$$
5		nfcsb1v	$$⊢\underset{\_}{Ⅎ}t⦋S/t⦌D$$
6		nfcv	$$⊢\underset{\_}{Ⅎ}t\underset{\dot{}}{\vee }$$
7		nfcv	$$⊢\underset{\_}{Ⅎ}t\left(\left(R\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }W\right)$$
8	5 6 7	nfov	$$⊢\underset{\_}{Ⅎ}t\left(⦋S/t⦌D\underset{\dot{}}{\vee }\left(\left(R\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }W\right)\right)$$
9	3 4 8	nfov	$$⊢\underset{\_}{Ⅎ}t\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\wedge }\left(⦋S/t⦌D\underset{\dot{}}{\vee }\left(\left(R\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }W\right)\right)\right)$$
10	9	a1i	$$⊢S\in A\to \underset{\_}{Ⅎ}t\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\wedge }\left(⦋S/t⦌D\underset{\dot{}}{\vee }\left(\left(R\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }W\right)\right)\right)$$
11		csbeq1a	$$⊢t=S\to D=⦋S/t⦌D$$
12		oveq2	$$⊢t=S\to R\underset{\dot{}}{\vee }t=R\underset{\dot{}}{\vee }S$$
13	12	oveq1d	$$⊢t=S\to \left(R\underset{\dot{}}{\vee }t\right)\underset{\dot{}}{\wedge }W=\left(R\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }W$$
14	11 13	oveq12d	$$⊢t=S\to D\underset{\dot{}}{\vee }\left(\left(R\underset{\dot{}}{\vee }t\right)\underset{\dot{}}{\wedge }W\right)=⦋S/t⦌D\underset{\dot{}}{\vee }\left(\left(R\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }W\right)$$
15	14	oveq2d	$$⊢t=S\to \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)=\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\wedge }\left(⦋S/t⦌D\underset{\dot{}}{\vee }\left(\left(R\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }W\right)\right)$$
16	10 15	csbiegf	$$⊢S\in A\to ⦋S/t⦌\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)=\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\wedge }\left(⦋S/t⦌D\underset{\dot{}}{\vee }\left(\left(R\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }W\right)\right)$$
17	1	csbeq2i	$$⊢⦋S/t⦌E=⦋S/t⦌\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)$$
18	16 17 2	3eqtr4g	$$⊢S\in A\to ⦋S/t⦌E=Y$$