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 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