Theorem neor 3042

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∨ wo 844   = wceq 1538   ≠ wne 2951

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 210  df-or 845  df-ne 2952

This theorem is referenced by:  frsn  5608  ord0eln0  6223  fimaxre  11622  fiminre  11625  prime  12102  h1datomi  29463  elat2  30222  bnj563  32242  divrngidl  35746  dmncan1  35794  lkrshp4  36684  cvrcmp  36859  leat2  36870  isat3  36883  2llnmat  37100  2lnat  37360