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

Metamath Proof Explorer

Theorem cdleme31sdnN

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

Ref Expression
Hypotheses cdleme31sdn.c 
|- C = ( ( s .\/ U ) ./\ ( Q .\/ ( ( P .\/ s ) ./\ W ) ) )
cdleme31sdn.d 
|- D = ( ( t .\/ U ) ./\ ( Q .\/ ( ( P .\/ t ) ./\ W ) ) )
cdleme31sdn.n 
|- N = if ( s .<_ ( P .\/ Q ) , I , C )
Assertion cdleme31sdnN 
|- N = if ( s .<_ ( P .\/ Q ) , I , [_ s / t ]_ D )

Proof

Step Hyp Ref Expression
1 cdleme31sdn.c 
 |-  C = ( ( s .\/ U ) ./\ ( Q .\/ ( ( P .\/ s ) ./\ W ) ) )
2 cdleme31sdn.d 
 |-  D = ( ( t .\/ U ) ./\ ( Q .\/ ( ( P .\/ t ) ./\ W ) ) )
3 cdleme31sdn.n 
 |-  N = if ( s .<_ ( P .\/ Q ) , I , C )
4 biid 
 |-  ( s .<_ ( P .\/ Q ) <-> s .<_ ( P .\/ Q ) )
5 2 1 cdleme31sc 
 |-  ( s e. _V -> [_ s / t ]_ D = C )
6 5 elv 
 |-  [_ s / t ]_ D = C
7 4 6 ifbieq2i 
 |-  if ( s .<_ ( P .\/ Q ) , I , [_ s / t ]_ D ) = if ( s .<_ ( P .\/ Q ) , I , C )
8 3 7 eqtr4i 
 |-  N = if ( s .<_ ( P .\/ Q ) , I , [_ s / t ]_ D )