Theorem dedth3v

Description: Weak deduction theorem for eliminating a hypothesis with 3 class variables. See comments in dedth2v . (Contributed by NM, 13-Aug-1999) (Proof shortened by Eric Schmidt, 28-Jul-2009)

	Ref	Expression
Hypotheses	dedth3v.1	⊢ ( 𝐴 = if ( 𝜑 , 𝐴 , 𝐷 ) → ( 𝜓 ↔ 𝜒 ) )
	dedth3v.2	⊢ ( 𝐵 = if ( 𝜑 , 𝐵 , 𝑅 ) → ( 𝜒 ↔ 𝜃 ) )
	dedth3v.3	⊢ ( 𝐶 = if ( 𝜑 , 𝐶 , 𝑆 ) → ( 𝜃 ↔ 𝜏 ) )
	dedth3v.4	⊢ 𝜏
Assertion	dedth3v	⊢ ( 𝜑 → 𝜓 )

Proof

Step	Hyp	Ref	Expression
1		dedth3v.1	⊢ ( 𝐴 = if ( 𝜑 , 𝐴 , 𝐷 ) → ( 𝜓 ↔ 𝜒 ) )
2		dedth3v.2	⊢ ( 𝐵 = if ( 𝜑 , 𝐵 , 𝑅 ) → ( 𝜒 ↔ 𝜃 ) )
3		dedth3v.3	⊢ ( 𝐶 = if ( 𝜑 , 𝐶 , 𝑆 ) → ( 𝜃 ↔ 𝜏 ) )
4		dedth3v.4	⊢ 𝜏
5	1 2 3 4	dedth3h	⊢ ( ( 𝜑 ∧ 𝜑 ∧ 𝜑 ) → 𝜓 )
6	5	3anidm12	⊢ ( ( 𝜑 ∧ 𝜑 ) → 𝜓 )
7	6	anidms	⊢ ( 𝜑 → 𝜓 )