Theorem elimifd

Description: Elimination of a conditional operator contained in a wff ch . (Contributed by Thierry Arnoux, 25-Jan-2017)

	Ref	Expression
Hypotheses	elimifd.1	⊢ ( 𝜑 → ( if ( 𝜓 , 𝐴 , 𝐵 ) = 𝐴 → ( 𝜒 ↔ 𝜃 ) ) )
	elimifd.2	⊢ ( 𝜑 → ( if ( 𝜓 , 𝐴 , 𝐵 ) = 𝐵 → ( 𝜒 ↔ 𝜏 ) ) )
Assertion	elimifd	⊢ ( 𝜑 → ( 𝜒 ↔ ( ( 𝜓 ∧ 𝜃 ) ∨ ( ¬ 𝜓 ∧ 𝜏 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		elimifd.1	⊢ ( 𝜑 → ( if ( 𝜓 , 𝐴 , 𝐵 ) = 𝐴 → ( 𝜒 ↔ 𝜃 ) ) )
2		elimifd.2	⊢ ( 𝜑 → ( if ( 𝜓 , 𝐴 , 𝐵 ) = 𝐵 → ( 𝜒 ↔ 𝜏 ) ) )
3		exmid	⊢ ( 𝜓 ∨ ¬ 𝜓 )
4	3	biantrur	⊢ ( 𝜒 ↔ ( ( 𝜓 ∨ ¬ 𝜓 ) ∧ 𝜒 ) )
5	4	a1i	⊢ ( 𝜑 → ( 𝜒 ↔ ( ( 𝜓 ∨ ¬ 𝜓 ) ∧ 𝜒 ) ) )
6		andir	⊢ ( ( ( 𝜓 ∨ ¬ 𝜓 ) ∧ 𝜒 ) ↔ ( ( 𝜓 ∧ 𝜒 ) ∨ ( ¬ 𝜓 ∧ 𝜒 ) ) )
7	6	a1i	⊢ ( 𝜑 → ( ( ( 𝜓 ∨ ¬ 𝜓 ) ∧ 𝜒 ) ↔ ( ( 𝜓 ∧ 𝜒 ) ∨ ( ¬ 𝜓 ∧ 𝜒 ) ) ) )
8		iftrue	⊢ ( 𝜓 → if ( 𝜓 , 𝐴 , 𝐵 ) = 𝐴 )
9	8 1	syl5	⊢ ( 𝜑 → ( 𝜓 → ( 𝜒 ↔ 𝜃 ) ) )
10	9	pm5.32d	⊢ ( 𝜑 → ( ( 𝜓 ∧ 𝜒 ) ↔ ( 𝜓 ∧ 𝜃 ) ) )
11		iffalse	⊢ ( ¬ 𝜓 → if ( 𝜓 , 𝐴 , 𝐵 ) = 𝐵 )
12	11 2	syl5	⊢ ( 𝜑 → ( ¬ 𝜓 → ( 𝜒 ↔ 𝜏 ) ) )
13	12	pm5.32d	⊢ ( 𝜑 → ( ( ¬ 𝜓 ∧ 𝜒 ) ↔ ( ¬ 𝜓 ∧ 𝜏 ) ) )
14	10 13	orbi12d	⊢ ( 𝜑 → ( ( ( 𝜓 ∧ 𝜒 ) ∨ ( ¬ 𝜓 ∧ 𝜒 ) ) ↔ ( ( 𝜓 ∧ 𝜃 ) ∨ ( ¬ 𝜓 ∧ 𝜏 ) ) ) )
15	5 7 14	3bitrd	⊢ ( 𝜑 → ( 𝜒 ↔ ( ( 𝜓 ∧ 𝜃 ) ∨ ( ¬ 𝜓 ∧ 𝜏 ) ) ) )