![]() |
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 867 | . 2 ⊢ (𝜓 → (𝜑 ∨ 𝜓)) | |
2 | orel1 888 | . 2 ⊢ (¬ 𝜑 → ((𝜑 ∨ 𝜓) → 𝜓)) | |
3 | 1, 2 | impbid2 225 | 1 ⊢ (¬ 𝜑 → (𝜓 ↔ (𝜑 ∨ 𝜓))) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 ∨ wo 846 |
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 206 df-or 847 |
This theorem is referenced by: biortn 937 pm5.55 948 pm5.75 1028 3bior1fd 1476 3bior2fd 1478 norasslem3 1538 euor 2612 euorv 2613 euor2 2614 eueq3 3674 unineq 4242 ifor 4545 difprsnss 4764 eqsn 4794 pr1eqbg 4819 disjprgw 5105 disjprg 5106 disjxun 5108 opthwiener 5476 opthprc 5701 frxp2 8081 swoord1 8686 brwdomn0 9512 fpwwe2lem12 10585 ne0gt0 11267 xrinfmss 13236 sumsplit 15660 sadadd2lem2 16337 coprm 16594 vdwlem11 16870 lvecvscan 20588 lvecvscan2 20589 mplcoe1 21454 mplcoe5 21457 maducoeval2 22005 xrsxmet 24188 itg2split 25130 plydiveu 25674 quotcan 25685 coseq1 25897 angrtmuld 26174 leibpilem2 26307 leibpi 26308 wilthlem2 26434 tgldimor 27486 tgcolg 27538 axcontlem7 27961 elntg2 27976 nb3grprlem2 28371 eupth2lem2 29205 eupth2lem3lem6 29219 nmlnogt0 29781 hvmulcan 30056 hvmulcan2 30057 rmounid 31465 disjunsn 31554 xrdifh 31725 bj-biorfi 35077 bj-snmoore 35613 nlpineqsn 35908 wl-ifp-ncond1 35964 itgaddnclem2 36166 biorfd 36717 elpadd0 38301 fsuppind 40794 or3or 42369 |
Copyright terms: Public domain | W3C validator |