Theorem cdleme31sc

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

	Ref	Expression
Hypotheses	cdleme31sc.c	⊢ 𝐶 = ( ( 𝑠 ∨ 𝑈 ) ∧ ( 𝑄 ∨ ( ( 𝑃 ∨ 𝑠 ) ∧ 𝑊 ) ) )
	cdleme31sc.x	⊢ 𝑋 = ( ( 𝑅 ∨ 𝑈 ) ∧ ( 𝑄 ∨ ( ( 𝑃 ∨ 𝑅 ) ∧ 𝑊 ) ) )
Assertion	cdleme31sc	⊢ ( 𝑅 ∈ 𝐴 → ⦋ 𝑅 / 𝑠 ⦌ 𝐶 = 𝑋 )

Proof

Step	Hyp	Ref	Expression
1		cdleme31sc.c	⊢ 𝐶 = ( ( 𝑠 ∨ 𝑈 ) ∧ ( 𝑄 ∨ ( ( 𝑃 ∨ 𝑠 ) ∧ 𝑊 ) ) )
2		cdleme31sc.x	⊢ 𝑋 = ( ( 𝑅 ∨ 𝑈 ) ∧ ( 𝑄 ∨ ( ( 𝑃 ∨ 𝑅 ) ∧ 𝑊 ) ) )
3		nfcvd	⊢ ( 𝑅 ∈ 𝐴 → Ⅎ 𝑠 ( ( 𝑅 ∨ 𝑈 ) ∧ ( 𝑄 ∨ ( ( 𝑃 ∨ 𝑅 ) ∧ 𝑊 ) ) ) )
4		oveq1	⊢ ( 𝑠 = 𝑅 → ( 𝑠 ∨ 𝑈 ) = ( 𝑅 ∨ 𝑈 ) )
5		oveq2	⊢ ( 𝑠 = 𝑅 → ( 𝑃 ∨ 𝑠 ) = ( 𝑃 ∨ 𝑅 ) )
6	5	oveq1d	⊢ ( 𝑠 = 𝑅 → ( ( 𝑃 ∨ 𝑠 ) ∧ 𝑊 ) = ( ( 𝑃 ∨ 𝑅 ) ∧ 𝑊 ) )
7	6	oveq2d	⊢ ( 𝑠 = 𝑅 → ( 𝑄 ∨ ( ( 𝑃 ∨ 𝑠 ) ∧ 𝑊 ) ) = ( 𝑄 ∨ ( ( 𝑃 ∨ 𝑅 ) ∧ 𝑊 ) ) )
8	4 7	oveq12d	⊢ ( 𝑠 = 𝑅 → ( ( 𝑠 ∨ 𝑈 ) ∧ ( 𝑄 ∨ ( ( 𝑃 ∨ 𝑠 ) ∧ 𝑊 ) ) ) = ( ( 𝑅 ∨ 𝑈 ) ∧ ( 𝑄 ∨ ( ( 𝑃 ∨ 𝑅 ) ∧ 𝑊 ) ) ) )
9	3 8	csbiegf	⊢ ( 𝑅 ∈ 𝐴 → ⦋ 𝑅 / 𝑠 ⦌ ( ( 𝑠 ∨ 𝑈 ) ∧ ( 𝑄 ∨ ( ( 𝑃 ∨ 𝑠 ) ∧ 𝑊 ) ) ) = ( ( 𝑅 ∨ 𝑈 ) ∧ ( 𝑄 ∨ ( ( 𝑃 ∨ 𝑅 ) ∧ 𝑊 ) ) ) )
10	1	csbeq2i	⊢ ⦋ 𝑅 / 𝑠 ⦌ 𝐶 = ⦋ 𝑅 / 𝑠 ⦌ ( ( 𝑠 ∨ 𝑈 ) ∧ ( 𝑄 ∨ ( ( 𝑃 ∨ 𝑠 ) ∧ 𝑊 ) ) )
11	9 10 2	3eqtr4g	⊢ ( 𝑅 ∈ 𝐴 → ⦋ 𝑅 / 𝑠 ⦌ 𝐶 = 𝑋 )