Description: Obsolete version of olcnd as of 13-Apr-2024. (Contributed by Giovanni Mascellani, 15-Sep-2017) (Proof modification is discouraged.) (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | olcnd.1 | |- ( ph -> ( ps \/ ch ) ) |
|
| olcnd.2 | |- ( ph -> -. ch ) |
||
| Assertion | unitreslOLD | |- ( ph -> ps ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | olcnd.1 | |- ( ph -> ( ps \/ ch ) ) |
|
| 2 | olcnd.2 | |- ( ph -> -. ch ) |
|
| 3 | orcom | |- ( ( ps \/ ch ) <-> ( ch \/ ps ) ) |
|
| 4 | df-or | |- ( ( ch \/ ps ) <-> ( -. ch -> ps ) ) |
|
| 5 | 3 4 | sylbb | |- ( ( ps \/ ch ) -> ( -. ch -> ps ) ) |
| 6 | 1 2 5 | sylc | |- ( ph -> ps ) |