Theorem dedth2h

Description: Weak deduction theorem eliminating two hypotheses. This theorem is simpler to use than dedth2v but requires that each hypothesis have exactly one class variable. See also comments in dedth . (Contributed by NM, 15-May-1999)

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

Proof

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