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 685 | . 2 ⊢ (𝜓 → (𝜑 ∨ 𝜓)) | |
2 | orel1 699 | . 2 ⊢ (¬ 𝜑 → ((𝜑 ∨ 𝜓) → 𝜓)) | |
3 | 1, 2 | impbid2 142 | 1 ⊢ (¬ 𝜑 → (𝜓 ↔ (𝜑 ∨ 𝜓))) |
Colors of variables: wff set class |
Syntax hints: ¬ wn 3 → wi 4 ↔ wb 104 ∨ wo 682 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-in2 589 ax-io 683 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: biortn 719 pm5.61 768 pm5.55dc 883 euor 2003 eueq3dc 2831 difprsnss 3628 exmidsssn 4095 opthprc 4560 frecabcl 6264 frecsuclem 6271 swoord1 6426 indpi 7118 enq0tr 7210 mulap0r 8345 mulge0 8349 leltap 8355 ap0gt0 8370 sumsplitdc 11169 coprm 11749 bdbl 12599 subctctexmid 13123 |
Copyright terms: Public domain | W3C validator |