Theorem dedth3h

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

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

Proof

Step	Hyp	Ref	Expression
1		dedth3h.1	⊢ ( 𝐴 = if ( 𝜑 , 𝐴 , 𝐷 ) → ( 𝜃 ↔ 𝜏 ) )
2		dedth3h.2	⊢ ( 𝐵 = if ( 𝜓 , 𝐵 , 𝑅 ) → ( 𝜏 ↔ 𝜂 ) )
3		dedth3h.3	⊢ ( 𝐶 = if ( 𝜒 , 𝐶 , 𝑆 ) → ( 𝜂 ↔ 𝜁 ) )
4		dedth3h.4	⊢ 𝜁
5	1	imbi2d	⊢ ( 𝐴 = if ( 𝜑 , 𝐴 , 𝐷 ) → ( ( ( 𝜓 ∧ 𝜒 ) → 𝜃 ) ↔ ( ( 𝜓 ∧ 𝜒 ) → 𝜏 ) ) )
6	2 3 4	dedth2h	⊢ ( ( 𝜓 ∧ 𝜒 ) → 𝜏 )
7	5 6	dedth	⊢ ( 𝜑 → ( ( 𝜓 ∧ 𝜒 ) → 𝜃 ) )
8	7	3impib	⊢ ( ( 𝜑 ∧ 𝜓 ∧ 𝜒 ) → 𝜃 )