![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
Mirrors > Home > MPE Home > Th. List > biorf | Structured 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 384 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | orel1 382 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | impbid2 204 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() ![]() ![]() |
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 185 df-or 370 |
This theorem is referenced by: biortn 406 pm5.61 712 pm5.55 892 3bior1fd 1325 3bior2fd 1327 cadanOLD 1435 euor 2319 euor2 2321 eueq3 3239 unineq 3707 ifor 3943 difprsnss 4116 disjprg 4395 disjxun 4397 opthwiener 4700 opthprc 4993 swoord1 7239 brwdomn0 7894 fpwwe2lem13 8919 ne0gt0 9589 xrinfmss 11382 sumsplit 13352 sadadd2lem2 13763 coprm 13903 vdwlem11 14169 lvecvscan 17314 lvecvscan2 17315 mplcoe1 17667 mplcoe5 17671 mplcoe2OLD 17673 maducoeval2 18577 xrsxmet 20517 itg2split 21359 plydiveu 21896 quotcan 21907 coseq1 22116 angrtmuld 22336 leibpilem2 22468 leibpi 22469 wilthlem2 22539 tgldimor 23089 tgcolg 23123 axcontlem7 23367 nb3graprlem2 23511 eupath2lem2 23750 eupath2lem3 23751 nmlnogt0 24348 hvmulcan 24625 hvmulcan2 24626 disjunsn 26086 xrdifh 26214 itgaddnclem2 28598 pr1eqbg 30268 bj-biorfi 32426 elpadd0 33776 |
Copyright terms: Public domain | W3C validator |