cases2

Description: Case disjunction according to the value of ph . (Contributed by BJ, 6-Apr-2019) (Proof shortened by Wolf Lammen, 28-Feb-2022)

		Ref	Expression
	Assertion	cases2	$⊢ ((φ \land ψ) \lor (\neg φ \land χ)) \leftrightarrow ((φ \to ψ) \land (\neg φ \to χ))$

Step	Hyp	Ref	Expression
1		pm4.83	$⊢ ((φ \to ((ψ \land φ) \lor (χ \land \neg φ))) \land (\neg φ \to ((ψ \land φ) \lor (χ \land \neg φ)))) \leftrightarrow ((ψ \land φ) \lor (χ \land \neg φ))$
2		dedlema	$⊢ φ \to (ψ \leftrightarrow ((ψ \land φ) \lor (χ \land \neg φ)))$
3	2	pm5.74i	$⊢ (φ \to ψ) \leftrightarrow (φ \to ((ψ \land φ) \lor (χ \land \neg φ)))$
4		dedlemb	$⊢ \neg φ \to (χ \leftrightarrow ((ψ \land φ) \lor (χ \land \neg φ)))$
5	4	pm5.74i	$⊢ (\neg φ \to χ) \leftrightarrow (\neg φ \to ((ψ \land φ) \lor (χ \land \neg φ)))$
6	3 5	anbi12i	$⊢ ((φ \to ψ) \land (\neg φ \to χ)) \leftrightarrow ((φ \to ((ψ \land φ) \lor (χ \land \neg φ))) \land (\neg φ \to ((ψ \land φ) \lor (χ \land \neg φ))))$
7		ancom	$⊢ (φ \land ψ) \leftrightarrow (ψ \land φ)$
8		ancom	$⊢ (\neg φ \land χ) \leftrightarrow (χ \land \neg φ)$
9	7 8	orbi12i	$⊢ ((φ \land ψ) \lor (\neg φ \land χ)) \leftrightarrow ((ψ \land φ) \lor (χ \land \neg φ))$
10	1 6 9	3bitr4ri	$⊢ ((φ \land ψ) \lor (\neg φ \land χ)) \leftrightarrow ((φ \to ψ) \land (\neg φ \to χ))$

Metamath Proof Explorer