Metamath Proof Explorer

Theorem or3or

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

Ref Expression
Assertion or3or 
|- ( ( ph \/ ps ) <-> ( ( ph /\ ps ) \/ ( ph /\ -. ps ) \/ ( -. ph /\ ps ) ) )

Proof

Step Hyp Ref Expression
1 excxor 
 |-  ( ( ph \/_ ps ) <-> ( ( ph /\ -. ps ) \/ ( -. ph /\ ps ) ) )
2 1 orbi2i 
 |-  ( ( ( ph /\ ps ) \/ ( ph \/_ ps ) ) <-> ( ( ph /\ ps ) \/ ( ( ph /\ -. ps ) \/ ( -. ph /\ ps ) ) ) )
3 orc 
 |-  ( ph -> ( ph \/ ps ) )
4 exmid 
 |-  ( ps \/ -. ps )
5 pm3.2 
 |-  ( ph -> ( ps -> ( ph /\ ps ) ) )
6 biimp 
 |-  ( ( ph <-> ps ) -> ( ph -> ps ) )
7 iman 
 |-  ( ( ph -> ps ) <-> -. ( ph /\ -. ps ) )
8 6 7 sylib 
 |-  ( ( ph <-> ps ) -> -. ( ph /\ -. ps ) )
9 8 con2i 
 |-  ( ( ph /\ -. ps ) -> -. ( ph <-> ps ) )
10 9 ex 
 |-  ( ph -> ( -. ps -> -. ( ph <-> ps ) ) )
11 df-xor 
 |-  ( ( ph \/_ ps ) <-> -. ( ph <-> ps ) )
12 11 bicomi 
 |-  ( -. ( ph <-> ps ) <-> ( ph \/_ ps ) )
13 10 12 imbitrdi 
 |-  ( ph -> ( -. ps -> ( ph \/_ ps ) ) )
14 5 13 orim12d 
 |-  ( ph -> ( ( ps \/ -. ps ) -> ( ( ph /\ ps ) \/ ( ph \/_ ps ) ) ) )
15 4 14 mpi 
 |-  ( ph -> ( ( ph /\ ps ) \/ ( ph \/_ ps ) ) )
16 3 15 2thd 
 |-  ( ph -> ( ( ph \/ ps ) <-> ( ( ph /\ ps ) \/ ( ph \/_ ps ) ) ) )
17 bicom 
 |-  ( ( ph <-> ps ) <-> ( ps <-> ph ) )
18 bibif 
 |-  ( -. ph -> ( ( ps <-> ph ) <-> -. ps ) )
19 17 18 bitrid 
 |-  ( -. ph -> ( ( ph <-> ps ) <-> -. ps ) )
20 19 con2bid 
 |-  ( -. ph -> ( ps <-> -. ( ph <-> ps ) ) )
21 20 12 bitrdi 
 |-  ( -. ph -> ( ps <-> ( ph \/_ ps ) ) )
22 biorf 
 |-  ( -. ph -> ( ps <-> ( ph \/ ps ) ) )
23 simpl 
 |-  ( ( ph /\ ps ) -> ph )
24 biorf 
 |-  ( -. ( ph /\ ps ) -> ( ( ph \/_ ps ) <-> ( ( ph /\ ps ) \/ ( ph \/_ ps ) ) ) )
25 23 24 nsyl5 
 |-  ( -. ph -> ( ( ph \/_ ps ) <-> ( ( ph /\ ps ) \/ ( ph \/_ ps ) ) ) )
26 21 22 25 3bitr3d 
 |-  ( -. ph -> ( ( ph \/ ps ) <-> ( ( ph /\ ps ) \/ ( ph \/_ ps ) ) ) )
27 16 26 pm2.61i 
 |-  ( ( ph \/ ps ) <-> ( ( ph /\ ps ) \/ ( ph \/_ ps ) ) )
28 3orass 
 |-  ( ( ( ph /\ ps ) \/ ( ph /\ -. ps ) \/ ( -. ph /\ ps ) ) <-> ( ( ph /\ ps ) \/ ( ( ph /\ -. ps ) \/ ( -. ph /\ ps ) ) ) )
29 2 27 28 3bitr4i 
 |-  ( ( ph \/ ps ) <-> ( ( ph /\ ps ) \/ ( ph /\ -. ps ) \/ ( -. ph /\ ps ) ) )