Theorem dedth4v

Description: Weak deduction theorem for eliminating a hypothesis with 4 class variables. See comments in dedth2v . (Contributed by NM, 21-Apr-2007) (Proof shortened by Eric Schmidt, 28-Jul-2009)

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

Proof

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