| Step |
Hyp |
Ref |
Expression |
| 1 |
|
eel12131.1 |
|- ( ph -> ps ) |
| 2 |
|
eel12131.2 |
|- ( ( ph /\ ch ) -> th ) |
| 3 |
|
eel12131.3 |
|- ( ( ph /\ ta ) -> et ) |
| 4 |
|
eel12131.4 |
|- ( ( ps /\ th /\ et ) -> ze ) |
| 5 |
4
|
3exp |
|- ( ps -> ( th -> ( et -> ze ) ) ) |
| 6 |
1 2 5
|
syl2imc |
|- ( ( ph /\ ch ) -> ( ph -> ( et -> ze ) ) ) |
| 7 |
6
|
ex |
|- ( ph -> ( ch -> ( ph -> ( et -> ze ) ) ) ) |
| 8 |
7
|
pm2.43b |
|- ( ch -> ( ph -> ( et -> ze ) ) ) |
| 9 |
8
|
com13 |
|- ( et -> ( ph -> ( ch -> ze ) ) ) |
| 10 |
3 9
|
syl |
|- ( ( ph /\ ta ) -> ( ph -> ( ch -> ze ) ) ) |
| 11 |
10
|
ex |
|- ( ph -> ( ta -> ( ph -> ( ch -> ze ) ) ) ) |
| 12 |
11
|
pm2.43b |
|- ( ta -> ( ph -> ( ch -> ze ) ) ) |
| 13 |
12
|
3imp231 |
|- ( ( ph /\ ch /\ ta ) -> ze ) |