This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )