| Step |
Hyp |
Ref |
Expression |
| 1 |
|
ccased.1 |
|- ( ph -> ( ( ps /\ ch ) -> et ) ) |
| 2 |
|
ccased.2 |
|- ( ph -> ( ( th /\ ch ) -> et ) ) |
| 3 |
|
ccased.3 |
|- ( ph -> ( ( ps /\ ta ) -> et ) ) |
| 4 |
|
ccased.4 |
|- ( ph -> ( ( th /\ ta ) -> et ) ) |
| 5 |
1
|
com12 |
|- ( ( ps /\ ch ) -> ( ph -> et ) ) |
| 6 |
2
|
com12 |
|- ( ( th /\ ch ) -> ( ph -> et ) ) |
| 7 |
3
|
com12 |
|- ( ( ps /\ ta ) -> ( ph -> et ) ) |
| 8 |
4
|
com12 |
|- ( ( th /\ ta ) -> ( ph -> et ) ) |
| 9 |
5 6 7 8
|
ccase |
|- ( ( ( ps \/ th ) /\ ( ch \/ ta ) ) -> ( ph -> et ) ) |
| 10 |
9
|
com12 |
|- ( ph -> ( ( ( ps \/ th ) /\ ( ch \/ ta ) ) -> et ) ) |