![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > neor | Structured version Visualization version GIF version |
Description: Logical OR with an equality. (Contributed by NM, 29-Apr-2007.) |
Ref | Expression |
---|---|
neor | ⊢ ((𝐴 = 𝐵 ∨ 𝜓) ↔ (𝐴 ≠ 𝐵 → 𝜓)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-or 847 | . 2 ⊢ ((𝐴 = 𝐵 ∨ 𝜓) ↔ (¬ 𝐴 = 𝐵 → 𝜓)) | |
2 | df-ne 2941 | . . 3 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐴 = 𝐵) | |
3 | 2 | imbi1i 350 | . 2 ⊢ ((𝐴 ≠ 𝐵 → 𝜓) ↔ (¬ 𝐴 = 𝐵 → 𝜓)) |
4 | 1, 3 | bitr4i 278 | 1 ⊢ ((𝐴 = 𝐵 ∨ 𝜓) ↔ (𝐴 ≠ 𝐵 → 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 ∨ wo 846 = wceq 1542 ≠ wne 2940 |
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 df-ne 2941 |
This theorem is referenced by: frsn 5720 ord0eln0 6373 fimaxre 12104 fiminre 12107 prime 12589 h1datomi 30565 elat2 31324 bnj563 33412 divrngidl 36533 dmncan1 36581 lkrshp4 37616 cvrcmp 37791 leat2 37802 isat3 37815 2llnmat 38033 2lnat 38293 |
Copyright terms: Public domain | W3C validator |