Theorem neor 3024

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 848	. 2 ⊢ ((𝐴 = 𝐵 ∨ 𝜓) ↔ (¬ 𝐴 = 𝐵 → 𝜓))
2		df-ne 2933	. . 3 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐴 = 𝐵)
3	2	imbi1i 349	. 2 ⊢ ((𝐴 ≠ 𝐵 → 𝜓) ↔ (¬ 𝐴 = 𝐵 → 𝜓))
4	1, 3	bitr4i 278	1 ⊢ ((𝐴 = 𝐵 ∨ 𝜓) ↔ (𝐴 ≠ 𝐵 → 𝜓))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∨ wo 847   = wceq 1541   ≠ wne 2932

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 848  df-ne 2933

This theorem is referenced by:  frsn  5712  ord0eln0  6373  fimaxre  12086  fiminre  12089  prime  12573  h1datomi  31656  elat2  32415  bnj563  34899  divrngidl  38229  dmncan1  38277  lkrshp4  39368  cvrcmp  39543  leat2  39554  isat3  39567  2llnmat  39784  2lnat  40044