Theorem or3or

Description: Decompose disjunction into three cases. (Contributed by RP, 5-Jul-2021)

	Ref	Expression
Assertion	or3or	⊢ ( ( 𝜑 ∨ 𝜓 ) ↔ ( ( 𝜑 ∧ 𝜓 ) ∨ ( 𝜑 ∧ ¬ 𝜓 ) ∨ ( ¬ 𝜑 ∧ 𝜓 ) ) )

Proof

Step	Hyp	Ref	Expression
1		excxor	⊢ ( ( 𝜑 ⊻ 𝜓 ) ↔ ( ( 𝜑 ∧ ¬ 𝜓 ) ∨ ( ¬ 𝜑 ∧ 𝜓 ) ) )
2	1	orbi2i	⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∨ ( 𝜑 ⊻ 𝜓 ) ) ↔ ( ( 𝜑 ∧ 𝜓 ) ∨ ( ( 𝜑 ∧ ¬ 𝜓 ) ∨ ( ¬ 𝜑 ∧ 𝜓 ) ) ) )
3		orc	⊢ ( 𝜑 → ( 𝜑 ∨ 𝜓 ) )
4		exmid	⊢ ( 𝜓 ∨ ¬ 𝜓 )
5		pm3.2	⊢ ( 𝜑 → ( 𝜓 → ( 𝜑 ∧ 𝜓 ) ) )
6		biimp	⊢ ( ( 𝜑 ↔ 𝜓 ) → ( 𝜑 → 𝜓 ) )
7		iman	⊢ ( ( 𝜑 → 𝜓 ) ↔ ¬ ( 𝜑 ∧ ¬ 𝜓 ) )
8	6 7	sylib	⊢ ( ( 𝜑 ↔ 𝜓 ) → ¬ ( 𝜑 ∧ ¬ 𝜓 ) )
9	8	con2i	⊢ ( ( 𝜑 ∧ ¬ 𝜓 ) → ¬ ( 𝜑 ↔ 𝜓 ) )
10	9	ex	⊢ ( 𝜑 → ( ¬ 𝜓 → ¬ ( 𝜑 ↔ 𝜓 ) ) )
11		df-xor	⊢ ( ( 𝜑 ⊻ 𝜓 ) ↔ ¬ ( 𝜑 ↔ 𝜓 ) )
12	11	bicomi	⊢ ( ¬ ( 𝜑 ↔ 𝜓 ) ↔ ( 𝜑 ⊻ 𝜓 ) )
13	10 12	syl6ib	⊢ ( 𝜑 → ( ¬ 𝜓 → ( 𝜑 ⊻ 𝜓 ) ) )
14	5 13	orim12d	⊢ ( 𝜑 → ( ( 𝜓 ∨ ¬ 𝜓 ) → ( ( 𝜑 ∧ 𝜓 ) ∨ ( 𝜑 ⊻ 𝜓 ) ) ) )
15	4 14	mpi	⊢ ( 𝜑 → ( ( 𝜑 ∧ 𝜓 ) ∨ ( 𝜑 ⊻ 𝜓 ) ) )
16	3 15	2thd	⊢ ( 𝜑 → ( ( 𝜑 ∨ 𝜓 ) ↔ ( ( 𝜑 ∧ 𝜓 ) ∨ ( 𝜑 ⊻ 𝜓 ) ) ) )
17		bicom	⊢ ( ( 𝜑 ↔ 𝜓 ) ↔ ( 𝜓 ↔ 𝜑 ) )
18		bibif	⊢ ( ¬ 𝜑 → ( ( 𝜓 ↔ 𝜑 ) ↔ ¬ 𝜓 ) )
19	17 18	syl5bb	⊢ ( ¬ 𝜑 → ( ( 𝜑 ↔ 𝜓 ) ↔ ¬ 𝜓 ) )
20	19	con2bid	⊢ ( ¬ 𝜑 → ( 𝜓 ↔ ¬ ( 𝜑 ↔ 𝜓 ) ) )
21	20 12	bitrdi	⊢ ( ¬ 𝜑 → ( 𝜓 ↔ ( 𝜑 ⊻ 𝜓 ) ) )
22		biorf	⊢ ( ¬ 𝜑 → ( 𝜓 ↔ ( 𝜑 ∨ 𝜓 ) ) )
23		simpl	⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝜑 )
24		biorf	⊢ ( ¬ ( 𝜑 ∧ 𝜓 ) → ( ( 𝜑 ⊻ 𝜓 ) ↔ ( ( 𝜑 ∧ 𝜓 ) ∨ ( 𝜑 ⊻ 𝜓 ) ) ) )
25	23 24	nsyl5	⊢ ( ¬ 𝜑 → ( ( 𝜑 ⊻ 𝜓 ) ↔ ( ( 𝜑 ∧ 𝜓 ) ∨ ( 𝜑 ⊻ 𝜓 ) ) ) )
26	21 22 25	3bitr3d	⊢ ( ¬ 𝜑 → ( ( 𝜑 ∨ 𝜓 ) ↔ ( ( 𝜑 ∧ 𝜓 ) ∨ ( 𝜑 ⊻ 𝜓 ) ) ) )
27	16 26	pm2.61i	⊢ ( ( 𝜑 ∨ 𝜓 ) ↔ ( ( 𝜑 ∧ 𝜓 ) ∨ ( 𝜑 ⊻ 𝜓 ) ) )
28		3orass	⊢ ( ( ( 𝜑 ∧ 𝜓 ) ∨ ( 𝜑 ∧ ¬ 𝜓 ) ∨ ( ¬ 𝜑 ∧ 𝜓 ) ) ↔ ( ( 𝜑 ∧ 𝜓 ) ∨ ( ( 𝜑 ∧ ¬ 𝜓 ) ∨ ( ¬ 𝜑 ∧ 𝜓 ) ) ) )
29	2 27 28	3bitr4i	⊢ ( ( 𝜑 ∨ 𝜓 ) ↔ ( ( 𝜑 ∧ 𝜓 ) ∨ ( 𝜑 ∧ ¬ 𝜓 ) ∨ ( ¬ 𝜑 ∧ 𝜓 ) ) )