Theorem cases

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

	Ref	Expression
Hypotheses	cases.1	⊢ ( 𝜑 → ( 𝜓 ↔ 𝜒 ) )
	cases.2	⊢ ( ¬ 𝜑 → ( 𝜓 ↔ 𝜃 ) )
Assertion	cases	⊢ ( 𝜓 ↔ ( ( 𝜑 ∧ 𝜒 ) ∨ ( ¬ 𝜑 ∧ 𝜃 ) ) )

Proof

Step	Hyp	Ref	Expression
1		cases.1	⊢ ( 𝜑 → ( 𝜓 ↔ 𝜒 ) )
2		cases.2	⊢ ( ¬ 𝜑 → ( 𝜓 ↔ 𝜃 ) )
3		exmid	⊢ ( 𝜑 ∨ ¬ 𝜑 )
4	3	biantrur	⊢ ( 𝜓 ↔ ( ( 𝜑 ∨ ¬ 𝜑 ) ∧ 𝜓 ) )
5		andir	⊢ ( ( ( 𝜑 ∨ ¬ 𝜑 ) ∧ 𝜓 ) ↔ ( ( 𝜑 ∧ 𝜓 ) ∨ ( ¬ 𝜑 ∧ 𝜓 ) ) )
6	1	pm5.32i	⊢ ( ( 𝜑 ∧ 𝜓 ) ↔ ( 𝜑 ∧ 𝜒 ) )
7	2	pm5.32i	⊢ ( ( ¬ 𝜑 ∧ 𝜓 ) ↔ ( ¬ 𝜑 ∧ 𝜃 ) )
8	6 7	orbi12i	⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∨ ( ¬ 𝜑 ∧ 𝜓 ) ) ↔ ( ( 𝜑 ∧ 𝜒 ) ∨ ( ¬ 𝜑 ∧ 𝜃 ) ) )
9	4 5 8	3bitri	⊢ ( 𝜓 ↔ ( ( 𝜑 ∧ 𝜒 ) ∨ ( ¬ 𝜑 ∧ 𝜃 ) ) )