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 398 | . 2 ⊢ (𝜓 → (𝜑 ∨ 𝜓)) | |
2 | orel1 396 | . 2 ⊢ (¬ 𝜑 → ((𝜑 ∨ 𝜓) → 𝜓)) | |
3 | 1, 2 | impbid2 215 | 1 ⊢ (¬ 𝜑 → (𝜓 ↔ (𝜑 ∨ 𝜓))) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ↔ wb 195 ∨ wo 382 |
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 196 df-or 384 |
This theorem is referenced by: biortn 420 pm5.61 745 pm5.55 937 pm5.75 974 3bior1fd 1430 3bior2fd 1432 euor 2500 euor2 2502 eueq3 3348 unineq 3836 ifor 4085 difprsnss 4270 eqsn 4301 disjprg 4578 disjxun 4581 opthwiener 4901 opthprc 5089 swoord1 7660 brwdomn0 8357 fpwwe2lem13 9343 ne0gt0 10021 xrinfmss 12012 sumsplit 14341 sadadd2lem2 15010 coprm 15261 vdwlem11 15533 lvecvscan 18932 lvecvscan2 18933 mplcoe1 19286 mplcoe5 19289 maducoeval2 20265 xrsxmet 22420 itg2split 23322 plydiveu 23857 quotcan 23868 coseq1 24078 angrtmuld 24338 leibpilem2 24468 leibpi 24469 wilthlem2 24595 tgldimor 25197 tgcolg 25249 axcontlem7 25650 nb3graprlem2 25981 eupath2lem2 26505 eupath2lem3 26506 nmlnogt0 27036 hvmulcan 27313 hvmulcan2 27314 disjunsn 28789 xrdifh 28932 bj-biorfi 31741 itgaddnclem2 32639 elpadd0 34113 or3or 37339 pr1eqbg 40313 nb3grprlem2 40609 eupth2lem2 41387 eupth2lem3lem6 41401 |
Copyright terms: Public domain | W3C validator |