![]() |
Mathbox for BJ |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > Mathboxes > bj-biorfi | Structured version Visualization version GIF version |
Description: This should be labeled "biorfi" while the current biorfi 937 should be labeled "biorfri". The dual of biorf 935 is not biantr 804 but iba 528 (and ibar 529). So there should also be a "biorfr". (Note that these four statements can actually be strengthened to biconditionals.) (Contributed by BJ, 26-Oct-2019.) (Proof modification is discouraged.) |
Ref | Expression |
---|---|
bj-biorfi.1 | ⊢ ¬ 𝜑 |
Ref | Expression |
---|---|
bj-biorfi | ⊢ (𝜓 ↔ (𝜑 ∨ 𝜓)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | bj-biorfi.1 | . 2 ⊢ ¬ 𝜑 | |
2 | biorf 935 | . 2 ⊢ (¬ 𝜑 → (𝜓 ↔ (𝜑 ∨ 𝜓))) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ (𝜓 ↔ (𝜑 ∨ 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ↔ 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: bj-falor 35548 |
Copyright terms: Public domain | W3C validator |