![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > biorf | 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 712 | . 2 ⊢ (𝜓 → (𝜑 ∨ 𝜓)) | |
2 | orel1 726 | . 2 ⊢ (¬ 𝜑 → ((𝜑 ∨ 𝜓) → 𝜓)) | |
3 | 1, 2 | impbid2 143 | 1 ⊢ (¬ 𝜑 → (𝜓 ↔ (𝜑 ∨ 𝜓))) |
Colors of variables: wff set class |
Syntax hints: ¬ wn 3 → wi 4 ↔ wb 105 ∨ wo 709 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-in2 616 ax-io 710 |
This theorem depends on definitions: df-bi 117 |
This theorem is referenced by: biortn 746 pm5.61 795 pm5.55dc 914 euor 2064 eueq3dc 2926 ifordc 3588 difprsnss 3745 exmidsssn 4220 opthprc 4695 frecabcl 6424 frecsuclem 6431 swoord1 6588 indpi 7371 enq0tr 7463 mulap0r 8602 mulge0 8606 leltap 8612 ap0gt0 8627 sumsplitdc 11472 coprm 12176 bdbl 14460 subctctexmid 15209 |
Copyright terms: Public domain | W3C validator |