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 842 | . 2 ⊢ ((𝐴 = 𝐵 ∨ 𝜓) ↔ (¬ 𝐴 = 𝐵 → 𝜓)) | |
2 | df-ne 3017 | . . 3 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐴 = 𝐵) | |
3 | 2 | imbi1i 351 | . 2 ⊢ ((𝐴 ≠ 𝐵 → 𝜓) ↔ (¬ 𝐴 = 𝐵 → 𝜓)) |
4 | 1, 3 | bitr4i 279 | 1 ⊢ ((𝐴 = 𝐵 ∨ 𝜓) ↔ (𝐴 ≠ 𝐵 → 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ↔ wb 207 ∨ wo 841 = wceq 1528 ≠ wne 3016 |
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 208 df-or 842 df-ne 3017 |
This theorem is referenced by: frsn 5633 ord0eln0 6239 fimaxre 11573 fimaxreOLD 11574 fiminre 11577 prime 12052 h1datomi 29286 elat2 30045 bnj563 31914 divrngidl 35189 dmncan1 35237 lkrshp4 36126 cvrcmp 36301 leat2 36312 isat3 36325 2llnmat 36542 2lnat 36802 |
Copyright terms: Public domain | W3C validator |