Theorem dedth3h

Description: Weak deduction theorem eliminating three hypotheses. See comments in dedth2h . (Contributed by NM, 15-May-1999)

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

Proof

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