Theorem cdleme31snd

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

	Ref	Expression
Hypotheses	cdleme31snd.d	|- D = ( ( t .\/ U ) ./\ ( Q .\/ ( ( P .\/ t ) ./\ W ) ) )
	cdleme31snd.n	|- N = ( ( v .\/ V ) ./\ ( P .\/ ( ( Q .\/ v ) ./\ W ) ) )
	cdleme31snd.e	|- E = ( ( O .\/ U ) ./\ ( Q .\/ ( ( P .\/ O ) ./\ W ) ) )
	cdleme31snd.o	|- O = ( ( S .\/ V ) ./\ ( P .\/ ( ( Q .\/ S ) ./\ W ) ) )
Assertion	cdleme31snd	|- ( S e. A -> [_ S / v ]_ [_ N / t ]_ D = E )

Proof

Step	Hyp	Ref	Expression
1		cdleme31snd.d	|- D = ( ( t .\/ U ) ./\ ( Q .\/ ( ( P .\/ t ) ./\ W ) ) )
2		cdleme31snd.n	|- N = ( ( v .\/ V ) ./\ ( P .\/ ( ( Q .\/ v ) ./\ W ) ) )
3		cdleme31snd.e	|- E = ( ( O .\/ U ) ./\ ( Q .\/ ( ( P .\/ O ) ./\ W ) ) )
4		cdleme31snd.o	|- O = ( ( S .\/ V ) ./\ ( P .\/ ( ( Q .\/ S ) ./\ W ) ) )
5		csbnestgw	|- ( S e. A -> [_ S / v ]_ [_ N / t ]_ D = [_ [_ S / v ]_ N / t ]_ D )
6	2 4	cdleme31sc	|- ( S e. A -> [_ S / v ]_ N = O )
7	6	csbeq1d	|- ( S e. A -> [_ [_ S / v ]_ N / t ]_ D = [_ O / t ]_ D )
8	4	ovexi	|- O e. _V
9	1 3	cdleme31sc	|- ( O e. _V -> [_ O / t ]_ D = E )
10	8 9	ax-mp	|- [_ O / t ]_ D = E
11	7 10	eqtrdi	|- ( S e. A -> [_ [_ S / v ]_ N / t ]_ D = E )
12	5 11	eqtrd	|- ( S e. A -> [_ S / v ]_ [_ N / t ]_ D = E )