Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > biorfi | Structured version Visualization version GIF version |
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 |
---|---|
biorfi.1 | ⊢ ¬ 𝜑 |
Ref | Expression |
---|---|
biorfi | ⊢ (𝜓 ↔ (𝜓 ∨ 𝜑)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | orc 865 | . 2 ⊢ (𝜓 → (𝜓 ∨ 𝜑)) | |
2 | biorfi.1 | . . 3 ⊢ ¬ 𝜑 | |
3 | pm2.53 849 | . . 3 ⊢ ((𝜓 ∨ 𝜑) → (¬ 𝜓 → 𝜑)) | |
4 | 2, 3 | mt3i 149 | . 2 ⊢ ((𝜓 ∨ 𝜑) → 𝜓) |
5 | 1, 4 | impbii 208 | 1 ⊢ (𝜓 ↔ (𝜓 ∨ 𝜑)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ↔ wb 205 ∨ wo 845 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 |
This theorem depends on definitions: df-bi 206 df-or 846 |
This theorem is referenced by: pm4.43 1021 dn1 1056 indifdirOLD 4225 un0 4330 opthprc 5662 imadif 6547 xrsupss 13093 mdegleb 25278 difrab2 30894 ind1a 32036 frxp2 33840 poimirlem30 35855 ifpdfan2 41283 ifpdfan 41286 ifpnot 41290 ifpid2 41291 uneqsn 41846 |
Copyright terms: Public domain | W3C validator |