Metamath Proof Explorer

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 imbitrdi ⊢ φ → ¬ ψ → φ ⊻ ψ
14 5 13 orim12d ⊢ φ → ψ ∨ ¬ ψ → φ ∧ ψ ∨ φ ⊻ ψ
15 4 14 mpi ⊢ φ → φ ∧ ψ ∨ φ ⊻ ψ
16 3 15 2thd ⊢ φ → φ ∨ ψ ↔ φ ∧ ψ ∨ φ ⊻ ψ
17 bicom ⊢ φ ↔ ψ ↔ ψ ↔ φ
18 bibif ⊢ ¬ φ → ψ ↔ φ ↔ ¬ ψ
19 17 18 bitrid ⊢ ¬ φ → φ ↔ ψ ↔ ¬ ψ
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 ⊢ φ ∨ ψ ↔ φ ∧ ψ ∨ φ ∧ ¬ ψ ∨ ¬ φ ∧ ψ