Theorem cases

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

	Ref	Expression
Hypotheses	cases.1	|- ( ph -> ( ps <-> ch ) )
	cases.2	|- ( -. ph -> ( ps <-> th ) )
Assertion	cases	|- ( ps <-> ( ( ph /\ ch ) \/ ( -. ph /\ th ) ) )

Proof

Step	Hyp	Ref	Expression
1		cases.1	|- ( ph -> ( ps <-> ch ) )
2		cases.2	|- ( -. ph -> ( ps <-> th ) )
3		exmid	|- ( ph \/ -. ph )
4	3	biantrur	|- ( ps <-> ( ( ph \/ -. ph ) /\ ps ) )
5		andir	|- ( ( ( ph \/ -. ph ) /\ ps ) <-> ( ( ph /\ ps ) \/ ( -. ph /\ ps ) ) )
6	1	pm5.32i	|- ( ( ph /\ ps ) <-> ( ph /\ ch ) )
7	2	pm5.32i	|- ( ( -. ph /\ ps ) <-> ( -. ph /\ th ) )
8	6 7	orbi12i	|- ( ( ( ph /\ ps ) \/ ( -. ph /\ ps ) ) <-> ( ( ph /\ ch ) \/ ( -. ph /\ th ) ) )
9	4 5 8	3bitri	|- ( ps <-> ( ( ph /\ ch ) \/ ( -. ph /\ th ) ) )