cases

Description: Case disjunction according to the value of ph . (Contributed by NM, 25-Apr-2019)

	Ref	Expression
Hypotheses	cases.1	$⊢ φ \to (ψ \leftrightarrow χ)$
	cases.2	$⊢ \neg φ \to (ψ \leftrightarrow θ)$
Assertion	cases	$⊢ ψ \leftrightarrow ((φ \land χ) \lor (\neg φ \land θ))$

Step	Hyp	Ref	Expression
1		cases.1	$⊢ φ \to (ψ \leftrightarrow χ)$
2		cases.2	$⊢ \neg φ \to (ψ \leftrightarrow θ)$
3		exmid	$⊢ (φ \lor \neg φ)$
4	3	biantrur	$⊢ ψ \leftrightarrow ((φ \lor \neg φ) \land ψ)$
5		andir	$⊢ ((φ \lor \neg φ) \land ψ) \leftrightarrow ((φ \land ψ) \lor (\neg φ \land ψ))$
6	1	pm5.32i	$⊢ (φ \land ψ) \leftrightarrow (φ \land χ)$
7	2	pm5.32i	$⊢ (\neg φ \land ψ) \leftrightarrow (\neg φ \land θ)$
8	6 7	orbi12i	$⊢ ((φ \land ψ) \lor (\neg φ \land ψ)) \leftrightarrow ((φ \land χ) \lor (\neg φ \land θ))$
9	4 5 8	3bitri	$⊢ ψ \leftrightarrow ((φ \land χ) \lor (\neg φ \land θ))$

Metamath Proof Explorer