Description: A self-implication does not imply the negation of a self-implication. Most general theorem of which bijust is an instance ( bijust0 and bj-bijust0ALT are therefore also instances of it). (Contributed by BJ, 7-Sep-2022)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | bj-bijust00 | |- -. ( ( ph -> ph ) -> -. ( ps -> ps ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | id | |- ( ph -> ph ) |
|
| 2 | id | |- ( ps -> ps ) |
|
| 3 | pm3.2im | |- ( ( ph -> ph ) -> ( ( ps -> ps ) -> -. ( ( ph -> ph ) -> -. ( ps -> ps ) ) ) ) |
|
| 4 | 1 2 3 | mp2 | |- -. ( ( ph -> ph ) -> -. ( ps -> ps ) ) |