Description: A wff is equivalent to its disjunction with falsehood. (Contributed by NM, 23-Mar-1995) (Proof shortened by Wolf Lammen, 16-Jul-2021)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | biorfi.1 | |- -. ph |
|
| Assertion | biorfi | |- ( ps <-> ( ps \/ ph ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | biorfi.1 | |- -. ph |
|
| 2 | orc | |- ( ps -> ( ps \/ ph ) ) |
|
| 3 | pm2.53 | |- ( ( ps \/ ph ) -> ( -. ps -> ph ) ) |
|
| 4 | 1 3 | mt3i | |- ( ( ps \/ ph ) -> ps ) |
| 5 | 2 4 | impbii | |- ( ps <-> ( ps \/ ph ) ) |