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 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 syl6bb ¬ φ ψ φ ψ
22 biorf ¬ φ ψ φ ψ
23 simpl φ ψ φ
24 23 con3i ¬ φ ¬ φ ψ
25 biorf ¬ φ ψ φ ψ φ ψ φ ψ
26 24 25 syl ¬ φ φ ψ φ ψ φ ψ
27 21 22 26 3bitr3d ¬ φ φ ψ φ ψ φ ψ
28 16 27 pm2.61i φ ψ φ ψ φ ψ
29 3orass φ ψ φ ¬ ψ ¬ φ ψ φ ψ φ ¬ ψ ¬ φ ψ
30 2 28 29 3bitr4i φ ψ φ ψ φ ¬ ψ ¬ φ ψ