| Step |
Hyp |
Ref |
Expression |
| 1 |
|
2if2.1 |
|- ( ( ph /\ ps ) -> D = A ) |
| 2 |
|
2if2.2 |
|- ( ( ph /\ -. ps /\ th ) -> D = B ) |
| 3 |
|
2if2.3 |
|- ( ( ph /\ -. ps /\ -. th ) -> D = C ) |
| 4 |
|
iftrue |
|- ( ps -> if ( ps , A , if ( th , B , C ) ) = A ) |
| 5 |
4
|
adantl |
|- ( ( ph /\ ps ) -> if ( ps , A , if ( th , B , C ) ) = A ) |
| 6 |
1 5
|
eqtr4d |
|- ( ( ph /\ ps ) -> D = if ( ps , A , if ( th , B , C ) ) ) |
| 7 |
2
|
3expa |
|- ( ( ( ph /\ -. ps ) /\ th ) -> D = B ) |
| 8 |
|
iftrue |
|- ( th -> if ( th , B , C ) = B ) |
| 9 |
8
|
adantl |
|- ( ( ( ph /\ -. ps ) /\ th ) -> if ( th , B , C ) = B ) |
| 10 |
7 9
|
eqtr4d |
|- ( ( ( ph /\ -. ps ) /\ th ) -> D = if ( th , B , C ) ) |
| 11 |
3
|
3expa |
|- ( ( ( ph /\ -. ps ) /\ -. th ) -> D = C ) |
| 12 |
|
iffalse |
|- ( -. th -> if ( th , B , C ) = C ) |
| 13 |
12
|
eqcomd |
|- ( -. th -> C = if ( th , B , C ) ) |
| 14 |
13
|
adantl |
|- ( ( ( ph /\ -. ps ) /\ -. th ) -> C = if ( th , B , C ) ) |
| 15 |
11 14
|
eqtrd |
|- ( ( ( ph /\ -. ps ) /\ -. th ) -> D = if ( th , B , C ) ) |
| 16 |
10 15
|
pm2.61dan |
|- ( ( ph /\ -. ps ) -> D = if ( th , B , C ) ) |
| 17 |
|
iffalse |
|- ( -. ps -> if ( ps , A , if ( th , B , C ) ) = if ( th , B , C ) ) |
| 18 |
17
|
adantl |
|- ( ( ph /\ -. ps ) -> if ( ps , A , if ( th , B , C ) ) = if ( th , B , C ) ) |
| 19 |
16 18
|
eqtr4d |
|- ( ( ph /\ -. ps ) -> D = if ( ps , A , if ( th , B , C ) ) ) |
| 20 |
6 19
|
pm2.61dan |
|- ( ph -> D = if ( ps , A , if ( th , B , C ) ) ) |