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=\left(s\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }\left(\left(P\underset{\dot{}}{\vee }s\right)\underset{\dot{}}{\wedge }W\right)\right)$$
	cdleme31sdn.d	$$⊢D=\left(t\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }\left(\left(P\underset{\dot{}}{\vee }t\right)\underset{\dot{}}{\wedge }W\right)\right)$$
	cdleme31sdn.n	$$⊢N=if\left(s\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right),I,C\right)$$
Assertion	cdleme31sdnN	$$⊢N=if\left(s\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right),I,⦋s/t⦌D\right)$$

Proof

Step	Hyp	Ref	Expression
1		cdleme31sdn.c	$$⊢C=\left(s\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }\left(\left(P\underset{\dot{}}{\vee }s\right)\underset{\dot{}}{\wedge }W\right)\right)$$
2		cdleme31sdn.d	$$⊢D=\left(t\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }\left(\left(P\underset{\dot{}}{\vee }t\right)\underset{\dot{}}{\wedge }W\right)\right)$$
3		cdleme31sdn.n	$$⊢N=if\left(s\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right),I,C\right)$$
4		biid	$$⊢s\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\leftrightarrow s\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)$$
5	2 1	cdleme31sc	$$⊢s\in \mathrm{V}\to ⦋s/t⦌D=C$$
6	5	elv	$$⊢⦋s/t⦌D=C$$
7	4 6	ifbieq2i	$$⊢if\left(s\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right),I,⦋s/t⦌D\right)=if\left(s\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right),I,C\right)$$
8	3 7	eqtr4i	$$⊢N=if\left(s\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right),I,⦋s/t⦌D\right)$$