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 | |
|
Assertion | biorfi | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | biorfi.1 | |
|
2 | orc | |
|
3 | pm2.53 | |
|
4 | 1 3 | mt3i | |
5 | 2 4 | impbii | |