Theorem elimdhyp

Description: Version of elimhyp where the hypothesis is deduced from the final antecedent. See divalg for an example of its use. (Contributed by Paul Chapman, 25-Mar-2008)

	Ref	Expression
Hypotheses	elimdhyp.1	⊢ ( 𝜑 → 𝜓 )
	elimdhyp.2	⊢ ( 𝐴 = if ( 𝜑 , 𝐴 , 𝐵 ) → ( 𝜓 ↔ 𝜒 ) )
	elimdhyp.3	⊢ ( 𝐵 = if ( 𝜑 , 𝐴 , 𝐵 ) → ( 𝜃 ↔ 𝜒 ) )
	elimdhyp.4	⊢ 𝜃
Assertion	elimdhyp	⊢ 𝜒

Proof

Step	Hyp	Ref	Expression
1		elimdhyp.1	⊢ ( 𝜑 → 𝜓 )
2		elimdhyp.2	⊢ ( 𝐴 = if ( 𝜑 , 𝐴 , 𝐵 ) → ( 𝜓 ↔ 𝜒 ) )
3		elimdhyp.3	⊢ ( 𝐵 = if ( 𝜑 , 𝐴 , 𝐵 ) → ( 𝜃 ↔ 𝜒 ) )
4		elimdhyp.4	⊢ 𝜃
5		iftrue	⊢ ( 𝜑 → if ( 𝜑 , 𝐴 , 𝐵 ) = 𝐴 )
6	5	eqcomd	⊢ ( 𝜑 → 𝐴 = if ( 𝜑 , 𝐴 , 𝐵 ) )
7	6 2	syl	⊢ ( 𝜑 → ( 𝜓 ↔ 𝜒 ) )
8	1 7	mpbid	⊢ ( 𝜑 → 𝜒 )
9		iffalse	⊢ ( ¬ 𝜑 → if ( 𝜑 , 𝐴 , 𝐵 ) = 𝐵 )
10	9	eqcomd	⊢ ( ¬ 𝜑 → 𝐵 = if ( 𝜑 , 𝐴 , 𝐵 ) )
11	10 3	syl	⊢ ( ¬ 𝜑 → ( 𝜃 ↔ 𝜒 ) )
12	4 11	mpbii	⊢ ( ¬ 𝜑 → 𝜒 )
13	8 12	pm2.61i	⊢ 𝜒