Step |
Hyp |
Ref |
Expression |
1 |
|
elimifd.1 |
|- ( ph -> ( if ( ps , A , B ) = A -> ( ch <-> th ) ) ) |
2 |
|
elimifd.2 |
|- ( ph -> ( if ( ps , A , B ) = B -> ( ch <-> ta ) ) ) |
3 |
|
exmid |
|- ( ps \/ -. ps ) |
4 |
3
|
biantrur |
|- ( ch <-> ( ( ps \/ -. ps ) /\ ch ) ) |
5 |
4
|
a1i |
|- ( ph -> ( ch <-> ( ( ps \/ -. ps ) /\ ch ) ) ) |
6 |
|
andir |
|- ( ( ( ps \/ -. ps ) /\ ch ) <-> ( ( ps /\ ch ) \/ ( -. ps /\ ch ) ) ) |
7 |
6
|
a1i |
|- ( ph -> ( ( ( ps \/ -. ps ) /\ ch ) <-> ( ( ps /\ ch ) \/ ( -. ps /\ ch ) ) ) ) |
8 |
|
iftrue |
|- ( ps -> if ( ps , A , B ) = A ) |
9 |
8 1
|
syl5 |
|- ( ph -> ( ps -> ( ch <-> th ) ) ) |
10 |
9
|
pm5.32d |
|- ( ph -> ( ( ps /\ ch ) <-> ( ps /\ th ) ) ) |
11 |
|
iffalse |
|- ( -. ps -> if ( ps , A , B ) = B ) |
12 |
11 2
|
syl5 |
|- ( ph -> ( -. ps -> ( ch <-> ta ) ) ) |
13 |
12
|
pm5.32d |
|- ( ph -> ( ( -. ps /\ ch ) <-> ( -. ps /\ ta ) ) ) |
14 |
10 13
|
orbi12d |
|- ( ph -> ( ( ( ps /\ ch ) \/ ( -. ps /\ ch ) ) <-> ( ( ps /\ th ) \/ ( -. ps /\ ta ) ) ) ) |
15 |
5 7 14
|
3bitrd |
|- ( ph -> ( ch <-> ( ( ps /\ th ) \/ ( -. ps /\ ta ) ) ) ) |