Theorem neor 3049

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 862	. 2 ⊢ ((𝐴 = 𝐵 ∨ 𝜓) ↔ (¬ 𝐴 = 𝐵 → 𝜓))
2		df-ne 2958	. . 3 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐴 = 𝐵)
3	2	imbi1i 352	. 2 ⊢ ((𝐴 ≠ 𝐵 → 𝜓) ↔ (¬ 𝐴 = 𝐵 → 𝜓))
4	1, 3	bitr4i 281	1 ⊢ ((𝐴 = 𝐵 ∨ 𝜓) ↔ (𝐴 ≠ 𝐵 → 𝜓))

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∨ wo 861   = wceq 1570   ≠ wne 2957

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-or 862  df-ne 2958

This theorem is used by:  frsn  5747  ord0eln0  6418  fimaxre  12187  fiminre  12190  prime  12706  h1datomi  32070  elat2  32829  bnj563  35261  divrngidl  38786  dmncan1  38834  dfdisjALTV5a  39559  dfeldisj5a  39570  lkrshp4  39989  cvrcmp  40164  leat2  40175  isat3  40188  2llnmat  40405  2lnat  40665  idomcanl  49270