Description: Obsolete version of ecase2d as of 19-Sep-2024. (Contributed by NM, 21-Apr-1994) (Proof shortened by Wolf Lammen, 22-Dec-2012) (New usage is discouraged.) (Proof modification is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | ecase2d.1 | |- ( ph -> ps ) |
|
| ecase2d.2 | |- ( ph -> -. ( ps /\ ch ) ) |
||
| ecase2d.3 | |- ( ph -> -. ( ps /\ th ) ) |
||
| ecase2d.4 | |- ( ph -> ( ta \/ ( ch \/ th ) ) ) |
||
| Assertion | ecase2dOLD | |- ( ph -> ta ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | ecase2d.1 | |- ( ph -> ps ) |
|
| 2 | ecase2d.2 | |- ( ph -> -. ( ps /\ ch ) ) |
|
| 3 | ecase2d.3 | |- ( ph -> -. ( ps /\ th ) ) |
|
| 4 | ecase2d.4 | |- ( ph -> ( ta \/ ( ch \/ th ) ) ) |
|
| 5 | idd | |- ( ph -> ( ta -> ta ) ) |
|
| 6 | 2 | pm2.21d | |- ( ph -> ( ( ps /\ ch ) -> ta ) ) |
| 7 | 1 6 | mpand | |- ( ph -> ( ch -> ta ) ) |
| 8 | 3 | pm2.21d | |- ( ph -> ( ( ps /\ th ) -> ta ) ) |
| 9 | 1 8 | mpand | |- ( ph -> ( th -> ta ) ) |
| 10 | 7 9 | jaod | |- ( ph -> ( ( ch \/ th ) -> ta ) ) |
| 11 | 5 10 4 | mpjaod | |- ( ph -> ta ) |