| 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 869 | . 2 ⊢ (𝜓 → (𝜑 ∨ 𝜓)) | |
| 2 | orel1 889 | . 2 ⊢ (¬ 𝜑 → ((𝜑 ∨ 𝜓) → 𝜓)) | |
| 3 | 1, 2 | impbid2 226 | 1 ⊢ (¬ 𝜑 → (𝜓 ↔ (𝜑 ∨ 𝜓))) |
| Colors of variables: wff setvar class |
| Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∨ wo 848 |
| 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 207 df-or 849 |
| This theorem is referenced by: biortn 938 biorfi 939 pm5.55 951 pm5.75 1031 3bior1fd 1477 3bior2fd 1479 norasslem3 1536 euor 2611 euorv 2612 euor2 2613 eueq3 3717 unineq 4288 ifor 4580 difprsnss 4799 eqsn 4829 pr1eqbg 4857 disjprg 5139 disjxun 5141 opthwiener 5519 swoord1 8777 brwdomn0 9609 fpwwe2lem12 10682 ne0gt0 11366 xrinfmss 13352 sumsplit 15804 sadadd2lem2 16487 coprm 16748 vdwlem11 17029 lvecvscan 21113 lvecvscan2 21114 mplcoe1 22055 mplcoe5 22058 maducoeval2 22646 xrsxmet 24831 itg2split 25784 plydiveu 26340 quotcan 26351 coseq1 26567 angrtmuld 26851 leibpilem2 26984 leibpi 26985 wilthlem2 27112 tgldimor 28510 tgcolg 28562 axcontlem7 28985 elntg2 29000 nb3grprlem2 29398 eupth2lem2 30238 eupth2lem3lem6 30252 nmlnogt0 30816 hvmulcan 31091 hvmulcan2 31092 rmounid 32514 disjunsn 32607 xrdifh 32782 bj-snmoore 37114 nlpineqsn 37409 wl-ifp-ncond1 37465 itgaddnclem2 37686 biorfd 38232 elpadd0 39811 fsuppind 42600 or3or 44036 |
| Copyright terms: Public domain | W3C validator |