![]() |
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 4245 un0 4350 opthprc 5696 imadif 6585 frxp2 8075 xrsupss 13227 mdegleb 25427 difrab2 31424 ind1a 32609 poimirlem30 36099 ifpdfan2 41717 ifpdfan 41720 ifpnot 41724 ifpid2 41725 uneqsn 42279 |
Copyright terms: Public domain | W3C validator |