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

Proof

Step	Hyp	Ref	Expression
1		pm4.83	⊢ ( ( ( 𝜑 → ( ( 𝜓 ∧ 𝜑 ) ∨ ( 𝜒 ∧ ¬ 𝜑 ) ) ) ∧ ( ¬ 𝜑 → ( ( 𝜓 ∧ 𝜑 ) ∨ ( 𝜒 ∧ ¬ 𝜑 ) ) ) ) ↔ ( ( 𝜓 ∧ 𝜑 ) ∨ ( 𝜒 ∧ ¬ 𝜑 ) ) )
2		dedlema	⊢ ( 𝜑 → ( 𝜓 ↔ ( ( 𝜓 ∧ 𝜑 ) ∨ ( 𝜒 ∧ ¬ 𝜑 ) ) ) )
3	2	pm5.74i	⊢ ( ( 𝜑 → 𝜓 ) ↔ ( 𝜑 → ( ( 𝜓 ∧ 𝜑 ) ∨ ( 𝜒 ∧ ¬ 𝜑 ) ) ) )
4		dedlemb	⊢ ( ¬ 𝜑 → ( 𝜒 ↔ ( ( 𝜓 ∧ 𝜑 ) ∨ ( 𝜒 ∧ ¬ 𝜑 ) ) ) )
5	4	pm5.74i	⊢ ( ( ¬ 𝜑 → 𝜒 ) ↔ ( ¬ 𝜑 → ( ( 𝜓 ∧ 𝜑 ) ∨ ( 𝜒 ∧ ¬ 𝜑 ) ) ) )
6	3 5	anbi12i	⊢ ( ( ( 𝜑 → 𝜓 ) ∧ ( ¬ 𝜑 → 𝜒 ) ) ↔ ( ( 𝜑 → ( ( 𝜓 ∧ 𝜑 ) ∨ ( 𝜒 ∧ ¬ 𝜑 ) ) ) ∧ ( ¬ 𝜑 → ( ( 𝜓 ∧ 𝜑 ) ∨ ( 𝜒 ∧ ¬ 𝜑 ) ) ) ) )
7		ancom	⊢ ( ( 𝜑 ∧ 𝜓 ) ↔ ( 𝜓 ∧ 𝜑 ) )
8		ancom	⊢ ( ( ¬ 𝜑 ∧ 𝜒 ) ↔ ( 𝜒 ∧ ¬ 𝜑 ) )
9	7 8	orbi12i	⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∨ ( ¬ 𝜑 ∧ 𝜒 ) ) ↔ ( ( 𝜓 ∧ 𝜑 ) ∨ ( 𝜒 ∧ ¬ 𝜑 ) ) )
10	1 6 9	3bitr4ri	⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∨ ( ¬ 𝜑 ∧ 𝜒 ) ) ↔ ( ( 𝜑 → 𝜓 ) ∧ ( ¬ 𝜑 → 𝜒 ) ) )