Step |
Hyp |
Ref |
Expression |
1 |
|
dfbi1 |
|- ( ( ph <-> ps ) <-> -. ( ( ph -> ps ) -> -. ( ps -> ph ) ) ) |
2 |
|
pm2.21 |
|- ( -. ( ps -> ph ) -> ( ( ps -> ph ) -> F. ) ) |
3 |
2
|
imim2i |
|- ( ( ( ph -> ps ) -> -. ( ps -> ph ) ) -> ( ( ph -> ps ) -> ( ( ps -> ph ) -> F. ) ) ) |
4 |
|
id |
|- ( -. ( ps -> ph ) -> -. ( ps -> ph ) ) |
5 |
|
falim |
|- ( F. -> -. ( ps -> ph ) ) |
6 |
4 5
|
ja |
|- ( ( ( ps -> ph ) -> F. ) -> -. ( ps -> ph ) ) |
7 |
6
|
imim2i |
|- ( ( ( ph -> ps ) -> ( ( ps -> ph ) -> F. ) ) -> ( ( ph -> ps ) -> -. ( ps -> ph ) ) ) |
8 |
3 7
|
impbii |
|- ( ( ( ph -> ps ) -> -. ( ps -> ph ) ) <-> ( ( ph -> ps ) -> ( ( ps -> ph ) -> F. ) ) ) |
9 |
8
|
notbii |
|- ( -. ( ( ph -> ps ) -> -. ( ps -> ph ) ) <-> -. ( ( ph -> ps ) -> ( ( ps -> ph ) -> F. ) ) ) |
10 |
|
pm2.21 |
|- ( -. ( ( ph -> ps ) -> ( ( ps -> ph ) -> F. ) ) -> ( ( ( ph -> ps ) -> ( ( ps -> ph ) -> F. ) ) -> F. ) ) |
11 |
|
ax-1 |
|- ( -. ( ( ph -> ps ) -> ( ( ps -> ph ) -> F. ) ) -> ( ( ( ( ph -> ps ) -> ( ( ps -> ph ) -> F. ) ) -> F. ) -> -. ( ( ph -> ps ) -> ( ( ps -> ph ) -> F. ) ) ) ) |
12 |
|
falim |
|- ( F. -> ( ( ( ( ph -> ps ) -> ( ( ps -> ph ) -> F. ) ) -> F. ) -> -. ( ( ph -> ps ) -> ( ( ps -> ph ) -> F. ) ) ) ) |
13 |
11 12
|
ja |
|- ( ( ( ( ph -> ps ) -> ( ( ps -> ph ) -> F. ) ) -> F. ) -> ( ( ( ( ph -> ps ) -> ( ( ps -> ph ) -> F. ) ) -> F. ) -> -. ( ( ph -> ps ) -> ( ( ps -> ph ) -> F. ) ) ) ) |
14 |
13
|
pm2.43i |
|- ( ( ( ( ph -> ps ) -> ( ( ps -> ph ) -> F. ) ) -> F. ) -> -. ( ( ph -> ps ) -> ( ( ps -> ph ) -> F. ) ) ) |
15 |
10 14
|
impbii |
|- ( -. ( ( ph -> ps ) -> ( ( ps -> ph ) -> F. ) ) <-> ( ( ( ph -> ps ) -> ( ( ps -> ph ) -> F. ) ) -> F. ) ) |
16 |
1 9 15
|
3bitri |
|- ( ( ph <-> ps ) <-> ( ( ( ph -> ps ) -> ( ( ps -> ph ) -> F. ) ) -> F. ) ) |