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 862 | . 2 ⊢ (𝜓 → (𝜑 ∨ 𝜓)) | |
2 | orel1 882 | . 2 ⊢ (¬ 𝜑 → ((𝜑 ∨ 𝜓) → 𝜓)) | |
3 | 1, 2 | impbid2 227 | 1 ⊢ (¬ 𝜑 → (𝜓 ↔ (𝜑 ∨ 𝜓))) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ↔ wb 207 ∨ wo 841 |
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 208 df-or 842 |
This theorem is referenced by: biortn 931 pm5.55 942 pm5.75 1022 3bior1fd 1466 3bior2fd 1468 norasslem3 1523 euor 2688 euorv 2689 euor2 2690 eueq3 3699 unineq 4251 ifor 4515 difprsnss 4724 eqsn 4754 pr1eqbg 4779 disjprgw 5052 disjprg 5053 disjxun 5055 opthwiener 5395 opthprc 5609 swoord1 8309 brwdomn0 9021 fpwwe2lem13 10052 ne0gt0 10733 xrinfmss 12691 sumsplit 15111 sadadd2lem2 15787 coprm 16043 vdwlem11 16315 lvecvscan 19812 lvecvscan2 19813 mplcoe1 20174 mplcoe5 20177 maducoeval2 21177 xrsxmet 23344 itg2split 24277 plydiveu 24814 quotcan 24825 coseq1 25037 angrtmuld 25313 leibpilem2 25446 leibpi 25447 wilthlem2 25573 tgldimor 26215 tgcolg 26267 axcontlem7 26683 elntg2 26698 nb3grprlem2 27090 eupth2lem2 27925 eupth2lem3lem6 27939 nmlnogt0 28501 hvmulcan 28776 hvmulcan2 28777 rmounid 30186 disjunsn 30272 xrdifh 30429 bj-biorfi 33814 bj-snmoore 34299 nlpineqsn 34571 itgaddnclem2 34832 elpadd0 36825 or3or 40249 |
Copyright terms: Public domain | W3C validator |