Theorem dedth2h

Description: Weak deduction theorem eliminating two hypotheses. This theorem is simpler to use than dedth2v but requires that each hypothesis have exactly one class variable. See also comments in dedth . (Contributed by NM, 15-May-1999)

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

Proof

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