Step |
Hyp |
Ref |
Expression |
1 |
|
ifeq3da.1 |
|- ( if ( ps , E , F ) = E -> C = G ) |
2 |
|
ifeq3da.2 |
|- ( if ( ps , E , F ) = F -> C = H ) |
3 |
|
ifeq3da.3 |
|- ( ph -> G = A ) |
4 |
|
ifeq3da.4 |
|- ( ph -> H = B ) |
5 |
|
iftrue |
|- ( ps -> if ( ps , E , F ) = E ) |
6 |
5 1
|
syl |
|- ( ps -> C = G ) |
7 |
6
|
adantl |
|- ( ( ph /\ ps ) -> C = G ) |
8 |
3
|
adantr |
|- ( ( ph /\ ps ) -> G = A ) |
9 |
7 8
|
eqtr2d |
|- ( ( ph /\ ps ) -> A = C ) |
10 |
|
iffalse |
|- ( -. ps -> if ( ps , E , F ) = F ) |
11 |
10 2
|
syl |
|- ( -. ps -> C = H ) |
12 |
11
|
adantl |
|- ( ( ph /\ -. ps ) -> C = H ) |
13 |
4
|
adantr |
|- ( ( ph /\ -. ps ) -> H = B ) |
14 |
12 13
|
eqtr2d |
|- ( ( ph /\ -. ps ) -> B = C ) |
15 |
9 14
|
ifeqda |
|- ( ph -> if ( ps , A , B ) = C ) |