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	⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∨ ( ¬ 𝜑 ∧ 𝜒 ) ) ↔ ( ( 𝜑 → 𝜓 ) ∧ ( ¬ 𝜑 → 𝜒 ) ) )

Proof

Step	Hyp	Ref	Expression
1		pm3.4	⊢ ( ( 𝜑 ∧ 𝜓 ) → ( 𝜑 → 𝜓 ) )
2		pm2.24	⊢ ( 𝜑 → ( ¬ 𝜑 → 𝜒 ) )
3	2	adantr	⊢ ( ( 𝜑 ∧ 𝜓 ) → ( ¬ 𝜑 → 𝜒 ) )
4	1 3	jca	⊢ ( ( 𝜑 ∧ 𝜓 ) → ( ( 𝜑 → 𝜓 ) ∧ ( ¬ 𝜑 → 𝜒 ) ) )
5		pm2.21	⊢ ( ¬ 𝜑 → ( 𝜑 → 𝜓 ) )
6	5	adantr	⊢ ( ( ¬ 𝜑 ∧ 𝜒 ) → ( 𝜑 → 𝜓 ) )
7		pm3.4	⊢ ( ( ¬ 𝜑 ∧ 𝜒 ) → ( ¬ 𝜑 → 𝜒 ) )
8	6 7	jca	⊢ ( ( ¬ 𝜑 ∧ 𝜒 ) → ( ( 𝜑 → 𝜓 ) ∧ ( ¬ 𝜑 → 𝜒 ) ) )
9	4 8	jaoi	⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∨ ( ¬ 𝜑 ∧ 𝜒 ) ) → ( ( 𝜑 → 𝜓 ) ∧ ( ¬ 𝜑 → 𝜒 ) ) )
10		pm2.27	⊢ ( 𝜑 → ( ( 𝜑 → 𝜓 ) → 𝜓 ) )
11	10	imdistani	⊢ ( ( 𝜑 ∧ ( 𝜑 → 𝜓 ) ) → ( 𝜑 ∧ 𝜓 ) )
12	11	orcd	⊢ ( ( 𝜑 ∧ ( 𝜑 → 𝜓 ) ) → ( ( 𝜑 ∧ 𝜓 ) ∨ ( ¬ 𝜑 ∧ 𝜒 ) ) )
13	12	adantrr	⊢ ( ( 𝜑 ∧ ( ( 𝜑 → 𝜓 ) ∧ ( ¬ 𝜑 → 𝜒 ) ) ) → ( ( 𝜑 ∧ 𝜓 ) ∨ ( ¬ 𝜑 ∧ 𝜒 ) ) )
14		pm2.27	⊢ ( ¬ 𝜑 → ( ( ¬ 𝜑 → 𝜒 ) → 𝜒 ) )
15	14	imdistani	⊢ ( ( ¬ 𝜑 ∧ ( ¬ 𝜑 → 𝜒 ) ) → ( ¬ 𝜑 ∧ 𝜒 ) )
16	15	olcd	⊢ ( ( ¬ 𝜑 ∧ ( ¬ 𝜑 → 𝜒 ) ) → ( ( 𝜑 ∧ 𝜓 ) ∨ ( ¬ 𝜑 ∧ 𝜒 ) ) )
17	16	adantrl	⊢ ( ( ¬ 𝜑 ∧ ( ( 𝜑 → 𝜓 ) ∧ ( ¬ 𝜑 → 𝜒 ) ) ) → ( ( 𝜑 ∧ 𝜓 ) ∨ ( ¬ 𝜑 ∧ 𝜒 ) ) )
18	13 17	pm2.61ian	⊢ ( ( ( 𝜑 → 𝜓 ) ∧ ( ¬ 𝜑 → 𝜒 ) ) → ( ( 𝜑 ∧ 𝜓 ) ∨ ( ¬ 𝜑 ∧ 𝜒 ) ) )
19	9 18	impbii	⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∨ ( ¬ 𝜑 ∧ 𝜒 ) ) ↔ ( ( 𝜑 → 𝜓 ) ∧ ( ¬ 𝜑 → 𝜒 ) ) )