Step |
Hyp |
Ref |
Expression |
1 |
|
pm2.45 |
|- ( -. ( ph \/ ps ) -> -. ph ) |
2 |
|
imnan |
|- ( ( -. ( ph \/ ps ) -> -. ph ) <-> -. ( -. ( ph \/ ps ) /\ ph ) ) |
3 |
1 2
|
mpbi |
|- -. ( -. ( ph \/ ps ) /\ ph ) |
4 |
3
|
biorfi |
|- ( ch <-> ( ch \/ ( -. ( ph \/ ps ) /\ ph ) ) ) |
5 |
|
orcom |
|- ( ( ch \/ ( -. ( ph \/ ps ) /\ ph ) ) <-> ( ( -. ( ph \/ ps ) /\ ph ) \/ ch ) ) |
6 |
|
ordir |
|- ( ( ( -. ( ph \/ ps ) /\ ph ) \/ ch ) <-> ( ( -. ( ph \/ ps ) \/ ch ) /\ ( ph \/ ch ) ) ) |
7 |
4 5 6
|
3bitri |
|- ( ch <-> ( ( -. ( ph \/ ps ) \/ ch ) /\ ( ph \/ ch ) ) ) |
8 |
|
pm4.45 |
|- ( ch <-> ( ch /\ ( ch \/ th ) ) ) |
9 |
|
anor |
|- ( ( ch /\ ( ch \/ th ) ) <-> -. ( -. ch \/ -. ( ch \/ th ) ) ) |
10 |
8 9
|
bitri |
|- ( ch <-> -. ( -. ch \/ -. ( ch \/ th ) ) ) |
11 |
10
|
orbi2i |
|- ( ( ph \/ ch ) <-> ( ph \/ -. ( -. ch \/ -. ( ch \/ th ) ) ) ) |
12 |
11
|
anbi2i |
|- ( ( ( -. ( ph \/ ps ) \/ ch ) /\ ( ph \/ ch ) ) <-> ( ( -. ( ph \/ ps ) \/ ch ) /\ ( ph \/ -. ( -. ch \/ -. ( ch \/ th ) ) ) ) ) |
13 |
|
anor |
|- ( ( ( -. ( ph \/ ps ) \/ ch ) /\ ( ph \/ -. ( -. ch \/ -. ( ch \/ th ) ) ) ) <-> -. ( -. ( -. ( ph \/ ps ) \/ ch ) \/ -. ( ph \/ -. ( -. ch \/ -. ( ch \/ th ) ) ) ) ) |
14 |
7 12 13
|
3bitrri |
|- ( -. ( -. ( -. ( ph \/ ps ) \/ ch ) \/ -. ( ph \/ -. ( -. ch \/ -. ( ch \/ th ) ) ) ) <-> ch ) |