Theorem neor 3025

Description: Logical OR with an equality. (Contributed by NM, 29-Apr-2007.)

Assertion

Ref	Expression
neor	⊢ ((𝐴 = 𝐵 ∨ 𝜓) ↔ (𝐴 ≠ 𝐵 → 𝜓))

Proof of Theorem neor

Step	Hyp	Ref	Expression
1		df-or 849	. 2 ⊢ ((𝐴 = 𝐵 ∨ 𝜓) ↔ (¬ 𝐴 = 𝐵 → 𝜓))
2		df-ne 2934	. . 3 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐴 = 𝐵)
3	2	imbi1i 349	. 2 ⊢ ((𝐴 ≠ 𝐵 → 𝜓) ↔ (¬ 𝐴 = 𝐵 → 𝜓))
4	1, 3	bitr4i 278	1 ⊢ ((𝐴 = 𝐵 ∨ 𝜓) ↔ (𝐴 ≠ 𝐵 → 𝜓))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∨ wo 848   = wceq 1542   ≠ wne 2933

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 849  df-ne 2934

This theorem is referenced by:  frsn  5712  ord0eln0  6373  fimaxre  12091  fiminre  12094  prime  12601  h1datomi  31667  elat2  32426  bnj563  34902  divrngidl  38363  dmncan1  38411  dfdisjALTV5a  39138  dfeldisj5a  39149  lkrshp4  39568  cvrcmp  39743  leat2  39754  isat3  39767  2llnmat  39984  2lnat  40244