Description: A wff is equivalent to its disjunction with falsehood. Theorem *4.74 of WhiteheadRussell p. 121. (Contributed by NM, 23-Mar-1995) (Proof shortened by Wolf Lammen, 18-Nov-2012)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | biorf | |- ( -. ph -> ( ps <-> ( ph \/ ps ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | olc | |- ( ps -> ( ph \/ ps ) ) |
|
| 2 | orel1 | |- ( -. ph -> ( ( ph \/ ps ) -> ps ) ) |
|
| 3 | 1 2 | impbid2 | |- ( -. ph -> ( ps <-> ( ph \/ ps ) ) ) |