elimifd

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

	Ref	Expression
Hypotheses	elimifd.1	$⊢ φ \to (if (ψ, A, B) = A \to (χ \leftrightarrow θ))$
	elimifd.2	$⊢ φ \to (if (ψ, A, B) = B \to (χ \leftrightarrow τ))$
Assertion	elimifd	$⊢ φ \to (χ \leftrightarrow ((ψ \land θ) \lor (\neg ψ \land τ)))$

Step	Hyp	Ref	Expression
1		elimifd.1	$⊢ φ \to (if (ψ, A, B) = A \to (χ \leftrightarrow θ))$
2		elimifd.2	$⊢ φ \to (if (ψ, A, B) = B \to (χ \leftrightarrow τ))$
3		exmid	$⊢ (ψ \lor \neg ψ)$
4	3	biantrur	$⊢ χ \leftrightarrow ((ψ \lor \neg ψ) \land χ)$
5	4	a1i	$⊢ φ \to (χ \leftrightarrow ((ψ \lor \neg ψ) \land χ))$
6		andir	$⊢ ((ψ \lor \neg ψ) \land χ) \leftrightarrow ((ψ \land χ) \lor (\neg ψ \land χ))$
7	6	a1i	$⊢ φ \to (((ψ \lor \neg ψ) \land χ) \leftrightarrow ((ψ \land χ) \lor (\neg ψ \land χ)))$
8		iftrue	$⊢ ψ \to if (ψ, A, B) = A$
9	8 1	syl5	$⊢ φ \to (ψ \to (χ \leftrightarrow θ))$
10	9	pm5.32d	$⊢ φ \to ((ψ \land χ) \leftrightarrow (ψ \land θ))$
11		iffalse	$⊢ \neg ψ \to if (ψ, A, B) = B$
12	11 2	syl5	$⊢ φ \to (\neg ψ \to (χ \leftrightarrow τ))$
13	12	pm5.32d	$⊢ φ \to ((\neg ψ \land χ) \leftrightarrow (\neg ψ \land τ))$
14	10 13	orbi12d	$⊢ φ \to (((ψ \land χ) \lor (\neg ψ \land χ)) \leftrightarrow ((ψ \land θ) \lor (\neg ψ \land τ)))$
15	5 7 14	3bitrd	$⊢ φ \to (χ \leftrightarrow ((ψ \land θ) \lor (\neg ψ \land τ)))$

Metamath Proof Explorer