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