Description: Obsolete version of ecase3ad as of 20-Sep-2024. (Contributed by NM, 24-May-2013) (Proof modification is discouraged.) (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | ecase3ad.1 | |- ( ph -> ( ps -> th ) ) |
|
| ecase3ad.2 | |- ( ph -> ( ch -> th ) ) |
||
| ecase3ad.3 | |- ( ph -> ( ( -. ps /\ -. ch ) -> th ) ) |
||
| Assertion | ecase3adOLD | |- ( ph -> th ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | ecase3ad.1 | |- ( ph -> ( ps -> th ) ) |
|
| 2 | ecase3ad.2 | |- ( ph -> ( ch -> th ) ) |
|
| 3 | ecase3ad.3 | |- ( ph -> ( ( -. ps /\ -. ch ) -> th ) ) |
|
| 4 | notnotr | |- ( -. -. ps -> ps ) |
|
| 5 | 4 1 | syl5 | |- ( ph -> ( -. -. ps -> th ) ) |
| 6 | notnotr | |- ( -. -. ch -> ch ) |
|
| 7 | 6 2 | syl5 | |- ( ph -> ( -. -. ch -> th ) ) |
| 8 | 5 7 3 | ecased | |- ( ph -> th ) |