Step |
Hyp |
Ref |
Expression |
1 |
|
idn1 |
|- (. ( ph <-> ps ) ->. ( ph <-> ps ) ). |
2 |
|
idn2 |
|- (. ( ph <-> ps ) ,. ( ch \/ ph ) ->. ( ch \/ ph ) ). |
3 |
|
pm1.4 |
|- ( ( ch \/ ph ) -> ( ph \/ ch ) ) |
4 |
2 3
|
e2 |
|- (. ( ph <-> ps ) ,. ( ch \/ ph ) ->. ( ph \/ ch ) ). |
5 |
|
orbi1 |
|- ( ( ph <-> ps ) -> ( ( ph \/ ch ) <-> ( ps \/ ch ) ) ) |
6 |
5
|
biimpd |
|- ( ( ph <-> ps ) -> ( ( ph \/ ch ) -> ( ps \/ ch ) ) ) |
7 |
1 4 6
|
e12 |
|- (. ( ph <-> ps ) ,. ( ch \/ ph ) ->. ( ps \/ ch ) ). |
8 |
|
pm1.4 |
|- ( ( ps \/ ch ) -> ( ch \/ ps ) ) |
9 |
7 8
|
e2 |
|- (. ( ph <-> ps ) ,. ( ch \/ ph ) ->. ( ch \/ ps ) ). |
10 |
9
|
in2 |
|- (. ( ph <-> ps ) ->. ( ( ch \/ ph ) -> ( ch \/ ps ) ) ). |
11 |
|
idn2 |
|- (. ( ph <-> ps ) ,. ( ch \/ ps ) ->. ( ch \/ ps ) ). |
12 |
|
pm1.4 |
|- ( ( ch \/ ps ) -> ( ps \/ ch ) ) |
13 |
11 12
|
e2 |
|- (. ( ph <-> ps ) ,. ( ch \/ ps ) ->. ( ps \/ ch ) ). |
14 |
5
|
biimprd |
|- ( ( ph <-> ps ) -> ( ( ps \/ ch ) -> ( ph \/ ch ) ) ) |
15 |
1 13 14
|
e12 |
|- (. ( ph <-> ps ) ,. ( ch \/ ps ) ->. ( ph \/ ch ) ). |
16 |
|
pm1.4 |
|- ( ( ph \/ ch ) -> ( ch \/ ph ) ) |
17 |
15 16
|
e2 |
|- (. ( ph <-> ps ) ,. ( ch \/ ps ) ->. ( ch \/ ph ) ). |
18 |
17
|
in2 |
|- (. ( ph <-> ps ) ->. ( ( ch \/ ps ) -> ( ch \/ ph ) ) ). |
19 |
|
impbi |
|- ( ( ( ch \/ ph ) -> ( ch \/ ps ) ) -> ( ( ( ch \/ ps ) -> ( ch \/ ph ) ) -> ( ( ch \/ ph ) <-> ( ch \/ ps ) ) ) ) |
20 |
10 18 19
|
e11 |
|- (. ( ph <-> ps ) ->. ( ( ch \/ ph ) <-> ( ch \/ ps ) ) ). |
21 |
20
|
in1 |
|- ( ( ph <-> ps ) -> ( ( ch \/ ph ) <-> ( ch \/ ps ) ) ) |