Theorem dedth2v

Description: Weak deduction theorem for eliminating a hypothesis with 2 class variables. Note: if the hypothesis can be separated into two hypotheses, each with one class variable, then dedth2h is simpler to use. See also comments in dedth . (Contributed by NM, 13-Aug-1999) (Proof shortened by Eric Schmidt, 28-Jul-2009)

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

Proof

Step	Hyp	Ref	Expression
1		dedth2v.1	$$⊢A=if\left(\phi ,A,C\right)\to \left(\psi \leftrightarrow \chi \right)$$
2		dedth2v.2	$$⊢B=if\left(\phi ,B,D\right)\to \left(\chi \leftrightarrow \theta \right)$$
3		dedth2v.3	$$⊢\theta$$
4	1 2 3	dedth2h	$$⊢\left(\phi \wedge \phi \right)\to \psi$$
5	4	anidms	$$⊢\phi \to \psi$$