Metamath Proof Explorer

Theorem cases2ALT

Description: Alternate proof of cases2 , not using dedlema or dedlemb . (Contributed by BJ, 6-Apr-2019) (Proof shortened by Wolf Lammen, 2-Jan-2020) (Proof modification is discouraged.) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		pm3.4	$⊢ (φ \land ψ) \to (φ \to ψ)$
2		pm2.24	$⊢ φ \to (\neg φ \to χ)$
3	2	adantr	$⊢ (φ \land ψ) \to (\neg φ \to χ)$
4	1 3	jca	$⊢ (φ \land ψ) \to ((φ \to ψ) \land (\neg φ \to χ))$
5		pm2.21	$⊢ \neg φ \to (φ \to ψ)$
6	5	adantr	$⊢ (\neg φ \land χ) \to (φ \to ψ)$
7		pm3.4	$⊢ (\neg φ \land χ) \to (\neg φ \to χ)$
8	6 7	jca	$⊢ (\neg φ \land χ) \to ((φ \to ψ) \land (\neg φ \to χ))$
9	4 8	jaoi	$⊢ ((φ \land ψ) \lor (\neg φ \land χ)) \to ((φ \to ψ) \land (\neg φ \to χ))$
10		pm2.27	$⊢ φ \to ((φ \to ψ) \to ψ)$
11	10	imdistani	$⊢ (φ \land (φ \to ψ)) \to (φ \land ψ)$
12	11	orcd	$⊢ (φ \land (φ \to ψ)) \to ((φ \land ψ) \lor (\neg φ \land χ))$
13	12	adantrr	$⊢ (φ \land ((φ \to ψ) \land (\neg φ \to χ))) \to ((φ \land ψ) \lor (\neg φ \land χ))$
14		pm2.27	$⊢ \neg φ \to ((\neg φ \to χ) \to χ)$
15	14	imdistani	$⊢ (\neg φ \land (\neg φ \to χ)) \to (\neg φ \land χ)$
16	15	olcd	$⊢ (\neg φ \land (\neg φ \to χ)) \to ((φ \land ψ) \lor (\neg φ \land χ))$
17	16	adantrl	$⊢ (\neg φ \land ((φ \to ψ) \land (\neg φ \to χ))) \to ((φ \land ψ) \lor (\neg φ \land χ))$
18	13 17	pm2.61ian	$⊢ ((φ \to ψ) \land (\neg φ \to χ)) \to ((φ \land ψ) \lor (\neg φ \land χ))$
19	9 18	impbii	$⊢ ((φ \land ψ) \lor (\neg φ \land χ)) \leftrightarrow ((φ \to ψ) \land (\neg φ \to χ))$