Theorem cdleme31se

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

	Ref	Expression
Hypotheses	cdleme31se.e	⊢ 𝐸 = ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝐷 ∨ ( ( 𝑠 ∨ 𝑇 ) ∧ 𝑊 ) ) )
	cdleme31se.y	⊢ 𝑌 = ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝐷 ∨ ( ( 𝑅 ∨ 𝑇 ) ∧ 𝑊 ) ) )
Assertion	cdleme31se	⊢ ( 𝑅 ∈ 𝐴 → ⦋ 𝑅 / 𝑠 ⦌ 𝐸 = 𝑌 )

Proof

Step	Hyp	Ref	Expression
1		cdleme31se.e	⊢ 𝐸 = ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝐷 ∨ ( ( 𝑠 ∨ 𝑇 ) ∧ 𝑊 ) ) )
2		cdleme31se.y	⊢ 𝑌 = ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝐷 ∨ ( ( 𝑅 ∨ 𝑇 ) ∧ 𝑊 ) ) )
3		nfcvd	⊢ ( 𝑅 ∈ 𝐴 → Ⅎ 𝑠 ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝐷 ∨ ( ( 𝑅 ∨ 𝑇 ) ∧ 𝑊 ) ) ) )
4		oveq1	⊢ ( 𝑠 = 𝑅 → ( 𝑠 ∨ 𝑇 ) = ( 𝑅 ∨ 𝑇 ) )
5	4	oveq1d	⊢ ( 𝑠 = 𝑅 → ( ( 𝑠 ∨ 𝑇 ) ∧ 𝑊 ) = ( ( 𝑅 ∨ 𝑇 ) ∧ 𝑊 ) )
6	5	oveq2d	⊢ ( 𝑠 = 𝑅 → ( 𝐷 ∨ ( ( 𝑠 ∨ 𝑇 ) ∧ 𝑊 ) ) = ( 𝐷 ∨ ( ( 𝑅 ∨ 𝑇 ) ∧ 𝑊 ) ) )
7	6	oveq2d	⊢ ( 𝑠 = 𝑅 → ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝐷 ∨ ( ( 𝑠 ∨ 𝑇 ) ∧ 𝑊 ) ) ) = ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝐷 ∨ ( ( 𝑅 ∨ 𝑇 ) ∧ 𝑊 ) ) ) )
8	3 7	csbiegf	⊢ ( 𝑅 ∈ 𝐴 → ⦋ 𝑅 / 𝑠 ⦌ ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝐷 ∨ ( ( 𝑠 ∨ 𝑇 ) ∧ 𝑊 ) ) ) = ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝐷 ∨ ( ( 𝑅 ∨ 𝑇 ) ∧ 𝑊 ) ) ) )
9	1	csbeq2i	⊢ ⦋ 𝑅 / 𝑠 ⦌ 𝐸 = ⦋ 𝑅 / 𝑠 ⦌ ( ( 𝑃 ∨ 𝑄 ) ∧ ( 𝐷 ∨ ( ( 𝑠 ∨ 𝑇 ) ∧ 𝑊 ) ) )
10	8 9 2	3eqtr4g	⊢ ( 𝑅 ∈ 𝐴 → ⦋ 𝑅 / 𝑠 ⦌ 𝐸 = 𝑌 )