![]() |
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 866 | . 2 ⊢ (𝜓 → (𝜑 ∨ 𝜓)) | |
2 | orel1 886 | . 2 ⊢ (¬ 𝜑 → ((𝜑 ∨ 𝜓) → 𝜓)) | |
3 | 1, 2 | impbid2 225 | 1 ⊢ (¬ 𝜑 → (𝜓 ↔ (𝜑 ∨ 𝜓))) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 ∨ wo 845 |
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 846 |
This theorem is referenced by: biortn 935 pm5.55 946 pm5.75 1026 3bior1fd 1471 3bior2fd 1473 norasslem3 1529 euor 2599 euorv 2600 euor2 2601 eueq3 3703 unineq 4276 ifor 4584 difprsnss 4804 eqsn 4834 pr1eqbg 4859 disjprgw 5144 disjprg 5145 disjxun 5147 opthwiener 5516 opthprc 5742 frxp2 8149 swoord1 8756 brwdomn0 9594 fpwwe2lem12 10667 ne0gt0 11351 xrinfmss 13324 sumsplit 15750 sadadd2lem2 16428 coprm 16685 vdwlem11 16963 lvecvscan 21011 lvecvscan2 21012 mplcoe1 21997 mplcoe5 22000 maducoeval2 22586 xrsxmet 24769 itg2split 25723 plydiveu 26278 quotcan 26289 coseq1 26504 angrtmuld 26785 leibpilem2 26918 leibpi 26919 wilthlem2 27046 tgldimor 28378 tgcolg 28430 axcontlem7 28853 elntg2 28868 nb3grprlem2 29266 eupth2lem2 30101 eupth2lem3lem6 30115 nmlnogt0 30679 hvmulcan 30954 hvmulcan2 30955 rmounid 32371 disjunsn 32463 xrdifh 32630 bj-biorfi 36188 bj-snmoore 36720 nlpineqsn 37015 wl-ifp-ncond1 37071 itgaddnclem2 37280 biorfd 37829 elpadd0 39409 fsuppind 41955 or3or 43592 |
Copyright terms: Public domain | W3C validator |