|   | 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 848 | . 2 ⊢ ((𝐴 = 𝐵 ∨ 𝜓) ↔ (¬ 𝐴 = 𝐵 → 𝜓)) | |
| 2 | df-ne 2940 | . . 3 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐴 = 𝐵) | |
| 3 | 2 | imbi1i 349 | . 2 ⊢ ((𝐴 ≠ 𝐵 → 𝜓) ↔ (¬ 𝐴 = 𝐵 → 𝜓)) | 
| 4 | 1, 3 | bitr4i 278 | 1 ⊢ ((𝐴 = 𝐵 ∨ 𝜓) ↔ (𝐴 ≠ 𝐵 → 𝜓)) | 
| Colors of variables: wff setvar class | 
| Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∨ wo 847 = wceq 1539 ≠ wne 2939 | 
| 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 207 df-or 848 df-ne 2940 | 
| This theorem is referenced by: frsn 5772 ord0eln0 6438 fimaxre 12213 fiminre 12216 prime 12701 h1datomi 31601 elat2 32360 bnj563 34758 divrngidl 38036 dmncan1 38084 lkrshp4 39110 cvrcmp 39285 leat2 39296 isat3 39309 2llnmat 39527 2lnat 39787 | 
| Copyright terms: Public domain | W3C validator |