# Metamath Proof Explorer

## Theorem or3or

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

Ref Expression
Assertion or3or ${⊢}\left({\phi }\vee {\psi }\right)↔\left(\left({\phi }\wedge {\psi }\right)\vee \left({\phi }\wedge ¬{\psi }\right)\vee \left(¬{\phi }\wedge {\psi }\right)\right)$

### Proof

Step Hyp Ref Expression
1 excxor ${⊢}\left({\phi }⊻{\psi }\right)↔\left(\left({\phi }\wedge ¬{\psi }\right)\vee \left(¬{\phi }\wedge {\psi }\right)\right)$
2 1 orbi2i ${⊢}\left(\left({\phi }\wedge {\psi }\right)\vee \left({\phi }⊻{\psi }\right)\right)↔\left(\left({\phi }\wedge {\psi }\right)\vee \left(\left({\phi }\wedge ¬{\psi }\right)\vee \left(¬{\phi }\wedge {\psi }\right)\right)\right)$
3 orc ${⊢}{\phi }\to \left({\phi }\vee {\psi }\right)$
4 exmid ${⊢}\left({\psi }\vee ¬{\psi }\right)$
5 pm3.2 ${⊢}{\phi }\to \left({\psi }\to \left({\phi }\wedge {\psi }\right)\right)$
6 biimp ${⊢}\left({\phi }↔{\psi }\right)\to \left({\phi }\to {\psi }\right)$
7 iman ${⊢}\left({\phi }\to {\psi }\right)↔¬\left({\phi }\wedge ¬{\psi }\right)$
8 6 7 sylib ${⊢}\left({\phi }↔{\psi }\right)\to ¬\left({\phi }\wedge ¬{\psi }\right)$
9 8 con2i ${⊢}\left({\phi }\wedge ¬{\psi }\right)\to ¬\left({\phi }↔{\psi }\right)$
10 9 ex ${⊢}{\phi }\to \left(¬{\psi }\to ¬\left({\phi }↔{\psi }\right)\right)$
11 df-xor ${⊢}\left({\phi }⊻{\psi }\right)↔¬\left({\phi }↔{\psi }\right)$
12 11 bicomi ${⊢}¬\left({\phi }↔{\psi }\right)↔\left({\phi }⊻{\psi }\right)$
13 10 12 syl6ib ${⊢}{\phi }\to \left(¬{\psi }\to \left({\phi }⊻{\psi }\right)\right)$
14 5 13 orim12d ${⊢}{\phi }\to \left(\left({\psi }\vee ¬{\psi }\right)\to \left(\left({\phi }\wedge {\psi }\right)\vee \left({\phi }⊻{\psi }\right)\right)\right)$
15 4 14 mpi ${⊢}{\phi }\to \left(\left({\phi }\wedge {\psi }\right)\vee \left({\phi }⊻{\psi }\right)\right)$
16 3 15 2thd ${⊢}{\phi }\to \left(\left({\phi }\vee {\psi }\right)↔\left(\left({\phi }\wedge {\psi }\right)\vee \left({\phi }⊻{\psi }\right)\right)\right)$
17 bicom ${⊢}\left({\phi }↔{\psi }\right)↔\left({\psi }↔{\phi }\right)$
18 bibif ${⊢}¬{\phi }\to \left(\left({\psi }↔{\phi }\right)↔¬{\psi }\right)$
19 17 18 syl5bb ${⊢}¬{\phi }\to \left(\left({\phi }↔{\psi }\right)↔¬{\psi }\right)$
20 19 con2bid ${⊢}¬{\phi }\to \left({\psi }↔¬\left({\phi }↔{\psi }\right)\right)$
21 20 12 syl6bb ${⊢}¬{\phi }\to \left({\psi }↔\left({\phi }⊻{\psi }\right)\right)$
22 biorf ${⊢}¬{\phi }\to \left({\psi }↔\left({\phi }\vee {\psi }\right)\right)$
23 simpl ${⊢}\left({\phi }\wedge {\psi }\right)\to {\phi }$
24 23 con3i ${⊢}¬{\phi }\to ¬\left({\phi }\wedge {\psi }\right)$
25 biorf ${⊢}¬\left({\phi }\wedge {\psi }\right)\to \left(\left({\phi }⊻{\psi }\right)↔\left(\left({\phi }\wedge {\psi }\right)\vee \left({\phi }⊻{\psi }\right)\right)\right)$
26 24 25 syl ${⊢}¬{\phi }\to \left(\left({\phi }⊻{\psi }\right)↔\left(\left({\phi }\wedge {\psi }\right)\vee \left({\phi }⊻{\psi }\right)\right)\right)$
27 21 22 26 3bitr3d ${⊢}¬{\phi }\to \left(\left({\phi }\vee {\psi }\right)↔\left(\left({\phi }\wedge {\psi }\right)\vee \left({\phi }⊻{\psi }\right)\right)\right)$
28 16 27 pm2.61i ${⊢}\left({\phi }\vee {\psi }\right)↔\left(\left({\phi }\wedge {\psi }\right)\vee \left({\phi }⊻{\psi }\right)\right)$
29 3orass ${⊢}\left(\left({\phi }\wedge {\psi }\right)\vee \left({\phi }\wedge ¬{\psi }\right)\vee \left(¬{\phi }\wedge {\psi }\right)\right)↔\left(\left({\phi }\wedge {\psi }\right)\vee \left(\left({\phi }\wedge ¬{\psi }\right)\vee \left(¬{\phi }\wedge {\psi }\right)\right)\right)$
30 2 28 29 3bitr4i ${⊢}\left({\phi }\vee {\psi }\right)↔\left(\left({\phi }\wedge {\psi }\right)\vee \left({\phi }\wedge ¬{\psi }\right)\vee \left(¬{\phi }\wedge {\psi }\right)\right)$