![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > biorf | Structured version Visualization version GIF version |
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 |
---|---|
biorf | ⊢ (¬ 𝜑 → (𝜓 ↔ (𝜑 ∨ 𝜓))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | olc 855 | . 2 ⊢ (𝜓 → (𝜑 ∨ 𝜓)) | |
2 | orel1 873 | . 2 ⊢ (¬ 𝜑 → ((𝜑 ∨ 𝜓) → 𝜓)) | |
3 | 1, 2 | impbid2 218 | 1 ⊢ (¬ 𝜑 → (𝜓 ↔ (𝜑 ∨ 𝜓))) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ↔ wb 198 ∨ wo 834 |
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 199 df-or 835 |
This theorem is referenced by: biortn 922 pm5.55 932 pm5.61 984 pm5.75 1012 3bior1fd 1455 3bior2fd 1457 euor 2645 euorv 2646 euor2 2648 eueq3 3618 unineq 4144 ifor 4405 difprsnss 4611 eqsn 4641 pr1eqbg 4666 disjprg 4930 disjxun 4932 opthwiener 5264 opthprc 5470 swoord1 8126 brwdomn0 8834 fpwwe2lem13 9868 ne0gt0 10551 xrinfmss 12525 sumsplit 14989 sadadd2lem2 15665 coprm 15917 vdwlem11 16189 lvecvscan 19617 lvecvscan2 19618 mplcoe1 19971 mplcoe5 19974 maducoeval2 20968 xrsxmet 23135 itg2split 24068 plydiveu 24605 quotcan 24616 coseq1 24828 angrtmuld 25102 leibpilem2 25236 leibpi 25237 wilthlem2 25363 tgldimor 26005 tgcolg 26057 axcontlem7 26474 elntg2 26489 nb3grprlem2 26881 eupth2lem2 27764 eupth2lem3lem6 27778 nmlnogt0 28366 hvmulcan 28643 hvmulcan2 28644 disjunsn 30127 xrdifh 30279 bj-biorfi 33474 bj-snmoore 33956 nlpineqsn 34170 itgaddnclem2 34432 elpadd0 36430 or3or 39775 |
Copyright terms: Public domain | W3C validator |