![]() |
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 2942 | . . 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 2941 |
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 2942 |
This theorem is referenced by: frsn 5764 ord0eln0 6420 fimaxre 12158 fiminre 12161 prime 12643 h1datomi 30834 elat2 31593 bnj563 33754 divrngidl 36896 dmncan1 36944 lkrshp4 37978 cvrcmp 38153 leat2 38164 isat3 38177 2llnmat 38395 2lnat 38655 |
Copyright terms: Public domain | W3C validator |