Step |
Hyp |
Ref |
Expression |
1 |
|
df-3or |
|- ( ( ph \/ ps \/ ch ) <-> ( ( ph \/ ps ) \/ ch ) ) |
2 |
|
df-or |
|- ( ( ( ph \/ ps ) \/ ch ) <-> ( -. ( ph \/ ps ) -> ch ) ) |
3 |
|
ioran |
|- ( -. ( ph \/ ps ) <-> ( -. ph /\ -. ps ) ) |
4 |
3
|
imbi1i |
|- ( ( -. ( ph \/ ps ) -> ch ) <-> ( ( -. ph /\ -. ps ) -> ch ) ) |
5 |
|
impexp |
|- ( ( ( -. ph /\ -. ps ) -> ch ) <-> ( -. ph -> ( -. ps -> ch ) ) ) |
6 |
4 5
|
bitri |
|- ( ( -. ( ph \/ ps ) -> ch ) <-> ( -. ph -> ( -. ps -> ch ) ) ) |
7 |
2 6
|
bitri |
|- ( ( ( ph \/ ps ) \/ ch ) <-> ( -. ph -> ( -. ps -> ch ) ) ) |
8 |
1 7
|
bitri |
|- ( ( ph \/ ps \/ ch ) <-> ( -. ph -> ( -. ps -> ch ) ) ) |