Theorem dedth4h

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

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

Proof

Step	Hyp	Ref	Expression
1		dedth4h.1	$$⊢A=if\left(\phi ,A,R\right)\to \left(\tau \leftrightarrow \eta \right)$$
2		dedth4h.2	$$⊢B=if\left(\psi ,B,S\right)\to \left(\eta \leftrightarrow \zeta \right)$$
3		dedth4h.3	$$⊢C=if\left(\chi ,C,F\right)\to \left(\zeta \leftrightarrow \sigma \right)$$
4		dedth4h.4	$$⊢D=if\left(\theta ,D,G\right)\to \left(\sigma \leftrightarrow \rho \right)$$
5		dedth4h.5	$$⊢\rho$$
6	1	imbi2d	$$⊢A=if\left(\phi ,A,R\right)\to \left(\left(\left(\chi \wedge \theta \right)\to \tau \right)\leftrightarrow \left(\left(\chi \wedge \theta \right)\to \eta \right)\right)$$
7	2	imbi2d	$$⊢B=if\left(\psi ,B,S\right)\to \left(\left(\left(\chi \wedge \theta \right)\to \eta \right)\leftrightarrow \left(\left(\chi \wedge \theta \right)\to \zeta \right)\right)$$
8	3 4 5	dedth2h	$$⊢\left(\chi \wedge \theta \right)\to \zeta$$
9	6 7 8	dedth2h	$$⊢\left(\phi \wedge \psi \right)\to \left(\left(\chi \wedge \theta \right)\to \tau \right)$$
10	9	imp	$$⊢\left(\left(\phi \wedge \psi \right)\wedge \left(\chi \wedge \theta \right)\right)\to \tau$$