Description: A wff is equivalent to its disjunction with falsehood. (Contributed by NM, 23-Mar-1995) (Proof shortened by Wolf Lammen, 16-Jul-2021) (Proof shortened by AV, 10-Aug-2025)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | biorfi.1 | |- -. ph |
|
| Assertion | biorfri | |- ( ps <-> ( ps \/ ph ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | biorfi.1 | |- -. ph |
|
| 2 | 1 | biorfi | |- ( ps <-> ( ph \/ ps ) ) |
| 3 | orcom | |- ( ( ph \/ ps ) <-> ( ps \/ ph ) ) |
|
| 4 | 2 3 | bitri | |- ( ps <-> ( ps \/ ph ) ) |