Step |
Hyp |
Ref |
Expression |
1 |
|
eelT01.1 |
|- ( T. -> ph ) |
2 |
|
eelT01.2 |
|- ps |
3 |
|
eelT01.3 |
|- ( ch -> th ) |
4 |
|
eelT01.4 |
|- ( ( ph /\ ps /\ th ) -> ta ) |
5 |
|
3anass |
|- ( ( T. /\ ps /\ ch ) <-> ( T. /\ ( ps /\ ch ) ) ) |
6 |
|
truan |
|- ( ( T. /\ ( ps /\ ch ) ) <-> ( ps /\ ch ) ) |
7 |
|
simpr |
|- ( ( ps /\ ch ) -> ch ) |
8 |
2
|
jctl |
|- ( ch -> ( ps /\ ch ) ) |
9 |
7 8
|
impbii |
|- ( ( ps /\ ch ) <-> ch ) |
10 |
5 6 9
|
3bitri |
|- ( ( T. /\ ps /\ ch ) <-> ch ) |
11 |
1 4
|
syl3an1 |
|- ( ( T. /\ ps /\ th ) -> ta ) |
12 |
3 11
|
syl3an3 |
|- ( ( T. /\ ps /\ ch ) -> ta ) |
13 |
10 12
|
sylbir |
|- ( ch -> ta ) |