Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > biorf | Structured version Visualization version Unicode 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 399 | . 2 | |
2 | orel1 397 | . 2 | |
3 | 1, 2 | impbid2 216 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wn 3 wi 4 wb 196 wo 383 |
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 197 df-or 385 |
This theorem is referenced by: biortn 421 pm5.61 749 pm5.55 939 pm5.75 978 3bior1fd 1438 3bior2fd 1440 euor 2512 euor2 2514 eueq3 3381 unineq 3877 ifor 4135 difprsnss 4329 eqsn 4361 pr1eqbg 4390 disjprg 4648 disjxun 4651 opthwiener 4976 opthprc 5167 swoord1 7773 brwdomn0 8474 fpwwe2lem13 9464 ne0gt0 10142 xrinfmss 12140 sumsplit 14499 sadadd2lem2 15172 coprm 15423 vdwlem11 15695 lvecvscan 19111 lvecvscan2 19112 mplcoe1 19465 mplcoe5 19468 maducoeval2 20446 xrsxmet 22612 itg2split 23516 plydiveu 24053 quotcan 24064 coseq1 24274 angrtmuld 24538 leibpilem2 24668 leibpi 24669 wilthlem2 24795 tgldimor 25397 tgcolg 25449 axcontlem7 25850 nb3grprlem2 26283 eupth2lem2 27079 eupth2lem3lem6 27093 nmlnogt0 27652 hvmulcan 27929 hvmulcan2 27930 disjunsn 29407 xrdifh 29542 bj-biorfi 32568 bj-snmoore 33068 itgaddnclem2 33469 elpadd0 35095 or3or 38319 |
Copyright terms: Public domain | W3C validator |