Theorem dedth3v

Description: Weak deduction theorem for eliminating a hypothesis with 3 class variables. See comments in dedth2v . (Contributed by NM, 13-Aug-1999) (Proof shortened by Eric Schmidt, 28-Jul-2009)

	Ref	Expression
Hypotheses	dedth3v.1	$$⊢A=if\left(\phi ,A,D\right)\to \left(\psi \leftrightarrow \chi \right)$$
	dedth3v.2	$$⊢B=if\left(\phi ,B,R\right)\to \left(\chi \leftrightarrow \theta \right)$$
	dedth3v.3	$$⊢C=if\left(\phi ,C,S\right)\to \left(\theta \leftrightarrow \tau \right)$$
	dedth3v.4	$$⊢\tau$$
Assertion	dedth3v	$$⊢\phi \to \psi$$

Proof

Step	Hyp	Ref	Expression
1		dedth3v.1	$$⊢A=if\left(\phi ,A,D\right)\to \left(\psi \leftrightarrow \chi \right)$$
2		dedth3v.2	$$⊢B=if\left(\phi ,B,R\right)\to \left(\chi \leftrightarrow \theta \right)$$
3		dedth3v.3	$$⊢C=if\left(\phi ,C,S\right)\to \left(\theta \leftrightarrow \tau \right)$$
4		dedth3v.4	$$⊢\tau$$
5	1 2 3 4	dedth3h	$$⊢\left(\phi \wedge \phi \wedge \phi \right)\to \psi$$
6	5	3anidm12	$$⊢\left(\phi \wedge \phi \right)\to \psi$$
7	6	anidms	$$⊢\phi \to \psi$$