Theorem neor 3075

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 843	. 2 ⊢ ((𝐴 = 𝐵 ∨ 𝜓) ↔ (¬ 𝐴 = 𝐵 → 𝜓))
2		df-ne 2984	. . 3 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐴 = 𝐵)
3	2	imbi1i 351	. 2 ⊢ ((𝐴 ≠ 𝐵 → 𝜓) ↔ (¬ 𝐴 = 𝐵 → 𝜓))
4	1, 3	bitr4i 279	1 ⊢ ((𝐴 = 𝐵 ∨ 𝜓) ↔ (𝐴 ≠ 𝐵 → 𝜓))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 207   ∨ wo 842   = wceq 1522   ≠ wne 2983

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 208  df-or 843  df-ne 2984

This theorem is referenced by:  frsn  5528  ord0eln0  6123  fimaxre  11434  fimaxreOLD  11435  fiminre  11438  prime  11913  h1datomi  29041  elat2  29800  bnj563  31623  divrngidl  34851  dmncan1  34899  lkrshp4  35788  cvrcmp  35963  leat2  35974  isat3  35987  2llnmat  36204  2lnat  36464