| Step |
Hyp |
Ref |
Expression |
| 1 |
|
elimhyp3v.1 |
|- ( A = if ( ph , A , D ) -> ( ph <-> ch ) ) |
| 2 |
|
elimhyp3v.2 |
|- ( B = if ( ph , B , R ) -> ( ch <-> th ) ) |
| 3 |
|
elimhyp3v.3 |
|- ( C = if ( ph , C , S ) -> ( th <-> ta ) ) |
| 4 |
|
elimhyp3v.4 |
|- ( D = if ( ph , A , D ) -> ( et <-> ze ) ) |
| 5 |
|
elimhyp3v.5 |
|- ( R = if ( ph , B , R ) -> ( ze <-> si ) ) |
| 6 |
|
elimhyp3v.6 |
|- ( S = if ( ph , C , S ) -> ( si <-> ta ) ) |
| 7 |
|
elimhyp3v.7 |
|- et |
| 8 |
|
iftrue |
|- ( ph -> if ( ph , A , D ) = A ) |
| 9 |
8
|
eqcomd |
|- ( ph -> A = if ( ph , A , D ) ) |
| 10 |
9 1
|
syl |
|- ( ph -> ( ph <-> ch ) ) |
| 11 |
|
iftrue |
|- ( ph -> if ( ph , B , R ) = B ) |
| 12 |
11
|
eqcomd |
|- ( ph -> B = if ( ph , B , R ) ) |
| 13 |
12 2
|
syl |
|- ( ph -> ( ch <-> th ) ) |
| 14 |
|
iftrue |
|- ( ph -> if ( ph , C , S ) = C ) |
| 15 |
14
|
eqcomd |
|- ( ph -> C = if ( ph , C , S ) ) |
| 16 |
15 3
|
syl |
|- ( ph -> ( th <-> ta ) ) |
| 17 |
10 13 16
|
3bitrd |
|- ( ph -> ( ph <-> ta ) ) |
| 18 |
17
|
ibi |
|- ( ph -> ta ) |
| 19 |
|
iffalse |
|- ( -. ph -> if ( ph , A , D ) = D ) |
| 20 |
19
|
eqcomd |
|- ( -. ph -> D = if ( ph , A , D ) ) |
| 21 |
20 4
|
syl |
|- ( -. ph -> ( et <-> ze ) ) |
| 22 |
|
iffalse |
|- ( -. ph -> if ( ph , B , R ) = R ) |
| 23 |
22
|
eqcomd |
|- ( -. ph -> R = if ( ph , B , R ) ) |
| 24 |
23 5
|
syl |
|- ( -. ph -> ( ze <-> si ) ) |
| 25 |
|
iffalse |
|- ( -. ph -> if ( ph , C , S ) = S ) |
| 26 |
25
|
eqcomd |
|- ( -. ph -> S = if ( ph , C , S ) ) |
| 27 |
26 6
|
syl |
|- ( -. ph -> ( si <-> ta ) ) |
| 28 |
21 24 27
|
3bitrd |
|- ( -. ph -> ( et <-> ta ) ) |
| 29 |
7 28
|
mpbii |
|- ( -. ph -> ta ) |
| 30 |
18 29
|
pm2.61i |
|- ta |