Description: A lemma for not-or-not elimination, in deduction form. (Contributed by Giovanni Mascellani, 19-Mar-2018)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | notornotel1.1 | |- ( ph -> -. ( -. ps \/ ch ) ) |
|
| Assertion | notornotel1 | |- ( ph -> ps ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | notornotel1.1 | |- ( ph -> -. ( -. ps \/ ch ) ) |
|
| 2 | ioran | |- ( -. ( -. ps \/ ch ) <-> ( -. -. ps /\ -. ch ) ) |
|
| 3 | 2 | biimpi | |- ( -. ( -. ps \/ ch ) -> ( -. -. ps /\ -. ch ) ) |
| 4 | simpl | |- ( ( -. -. ps /\ -. ch ) -> -. -. ps ) |
|
| 5 | notnotr | |- ( -. -. ps -> ps ) |
|
| 6 | 3 4 5 | 3syl | |- ( -. ( -. ps \/ ch ) -> ps ) |
| 7 | 1 6 | syl | |- ( ph -> ps ) |