Step |
Hyp |
Ref |
Expression |
1 |
|
dfbi1 |
|- ( ( ph <-> ps ) <-> -. ( ( ph -> ps ) -> -. ( ps -> ph ) ) ) |
2 |
|
imor |
|- ( ( ph -> ps ) <-> ( -. ph \/ ps ) ) |
3 |
|
imor |
|- ( ( ps -> ph ) <-> ( -. ps \/ ph ) ) |
4 |
3
|
notbii |
|- ( -. ( ps -> ph ) <-> -. ( -. ps \/ ph ) ) |
5 |
2 4
|
imbi12i |
|- ( ( ( ph -> ps ) -> -. ( ps -> ph ) ) <-> ( ( -. ph \/ ps ) -> -. ( -. ps \/ ph ) ) ) |
6 |
5
|
notbii |
|- ( -. ( ( ph -> ps ) -> -. ( ps -> ph ) ) <-> -. ( ( -. ph \/ ps ) -> -. ( -. ps \/ ph ) ) ) |
7 |
|
pm4.62 |
|- ( ( ( -. ph \/ ps ) -> -. ( -. ps \/ ph ) ) <-> ( -. ( -. ph \/ ps ) \/ -. ( -. ps \/ ph ) ) ) |
8 |
7
|
notbii |
|- ( -. ( ( -. ph \/ ps ) -> -. ( -. ps \/ ph ) ) <-> -. ( -. ( -. ph \/ ps ) \/ -. ( -. ps \/ ph ) ) ) |
9 |
1 6 8
|
3bitri |
|- ( ( ph <-> ps ) <-> -. ( -. ( -. ph \/ ps ) \/ -. ( -. ps \/ ph ) ) ) |