![]() |
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 846 | . 2 ⊢ ((𝐴 = 𝐵 ∨ 𝜓) ↔ (¬ 𝐴 = 𝐵 → 𝜓)) | |
2 | df-ne 2944 | . . 3 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐴 = 𝐵) | |
3 | 2 | imbi1i 349 | . 2 ⊢ ((𝐴 ≠ 𝐵 → 𝜓) ↔ (¬ 𝐴 = 𝐵 → 𝜓)) |
4 | 1, 3 | bitr4i 277 | 1 ⊢ ((𝐴 = 𝐵 ∨ 𝜓) ↔ (𝐴 ≠ 𝐵 → 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 ∨ wo 845 = wceq 1541 ≠ wne 2943 |
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 df-ne 2944 |
This theorem is referenced by: frsn 5719 ord0eln0 6372 fimaxre 12098 fiminre 12101 prime 12583 h1datomi 30470 elat2 31229 bnj563 33295 divrngidl 36477 dmncan1 36525 lkrshp4 37560 cvrcmp 37735 leat2 37746 isat3 37759 2llnmat 37977 2lnat 38237 |
Copyright terms: Public domain | W3C validator |