Theorem dedth4h

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

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

Proof

Step	Hyp	Ref	Expression
1		dedth4h.1	⊢ ( 𝐴 = if ( 𝜑 , 𝐴 , 𝑅 ) → ( 𝜏 ↔ 𝜂 ) )
2		dedth4h.2	⊢ ( 𝐵 = if ( 𝜓 , 𝐵 , 𝑆 ) → ( 𝜂 ↔ 𝜁 ) )
3		dedth4h.3	⊢ ( 𝐶 = if ( 𝜒 , 𝐶 , 𝐹 ) → ( 𝜁 ↔ 𝜎 ) )
4		dedth4h.4	⊢ ( 𝐷 = if ( 𝜃 , 𝐷 , 𝐺 ) → ( 𝜎 ↔ 𝜌 ) )
5		dedth4h.5	⊢ 𝜌
6	1	imbi2d	⊢ ( 𝐴 = if ( 𝜑 , 𝐴 , 𝑅 ) → ( ( ( 𝜒 ∧ 𝜃 ) → 𝜏 ) ↔ ( ( 𝜒 ∧ 𝜃 ) → 𝜂 ) ) )
7	2	imbi2d	⊢ ( 𝐵 = if ( 𝜓 , 𝐵 , 𝑆 ) → ( ( ( 𝜒 ∧ 𝜃 ) → 𝜂 ) ↔ ( ( 𝜒 ∧ 𝜃 ) → 𝜁 ) ) )
8	3 4 5	dedth2h	⊢ ( ( 𝜒 ∧ 𝜃 ) → 𝜁 )
9	6 7 8	dedth2h	⊢ ( ( 𝜑 ∧ 𝜓 ) → ( ( 𝜒 ∧ 𝜃 ) → 𝜏 ) )
10	9	imp	⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∧ ( 𝜒 ∧ 𝜃 ) ) → 𝜏 )