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 844 | . 2 ⊢ ((𝐴 = 𝐵 ∨ 𝜓) ↔ (¬ 𝐴 = 𝐵 → 𝜓)) | |
2 | df-ne 3017 | . . 3 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐴 = 𝐵) | |
3 | 2 | imbi1i 352 | . 2 ⊢ ((𝐴 ≠ 𝐵 → 𝜓) ↔ (¬ 𝐴 = 𝐵 → 𝜓)) |
4 | 1, 3 | bitr4i 280 | 1 ⊢ ((𝐴 = 𝐵 ∨ 𝜓) ↔ (𝐴 ≠ 𝐵 → 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ↔ wb 208 ∨ wo 843 = wceq 1533 ≠ 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 209 df-or 844 df-ne 3017 |
This theorem is referenced by: frsn 5638 ord0eln0 6244 fimaxre 11583 fimaxreOLD 11584 fiminre 11587 prime 12062 h1datomi 29357 elat2 30116 bnj563 32014 divrngidl 35305 dmncan1 35353 lkrshp4 36243 cvrcmp 36418 leat2 36429 isat3 36442 2llnmat 36659 2lnat 36919 |
Copyright terms: Public domain | W3C validator |