Theorem necon3abid 2859

Description: Deduction from equality to inequality. (Contributed by NM, 21-Mar-2007.)

Hypothesis

Ref	Expression
necon3abid.1	⊢ (𝜑 → (𝐴 = 𝐵 ↔ 𝜓))

Assertion

Ref	Expression
necon3abid	⊢ (𝜑 → (𝐴 ≠ 𝐵 ↔ ¬ 𝜓))

Proof of Theorem necon3abid

Step	Hyp	Ref	Expression
1		df-ne 2824	. 2 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐴 = 𝐵)
2		necon3abid.1	. . 3 ⊢ (𝜑 → (𝐴 = 𝐵 ↔ 𝜓))
3	2	notbid 307	. 2 ⊢ (𝜑 → (¬ 𝐴 = 𝐵 ↔ ¬ 𝜓))
4	1, 3	syl5bb 272	1 ⊢ (𝜑 → (𝐴 ≠ 𝐵 ↔ ¬ 𝜓))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 196   = wceq 1523   ≠ wne 2823

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 197  df-ne 2824

This theorem is referenced by:  necon3bbid  2860  necon2abid  2865  foconst  6164  fndmdif  6361  suppsnop  7354  om00el  7701  oeoa  7722  cardsdom2  8852  mulne0b  10706  crne0  11051  expneg  12908  hashsdom  13208  prprrab  13293  gcdn0gt0  15286  cncongr2  15429  pltval3  17014  mulgnegnn  17598  drngmulne0  18817  lvecvsn0  19157  domnmuln0  19346  mvrf1  19473  connsub  21272  pthaus  21489  xkohaus  21504  bndth  22804  lebnumlem1  22807  dvcobr  23754  dvcnvlem  23784  mdegle0  23882  coemulhi  24055  vieta1lem1  24110  vieta1lem2  24111  aalioulem2  24133  cosne0  24321  atandm3  24650  wilthlem2  24840  issqf  24907  mumullem2  24951  dchrptlem3  25036  lgseisenlem3  25147  brbtwn2  25830  colinearalg  25835  vdn0conngrumgrv2  27174  vdgn1frgrv2  27276  nmlno0lem  27776  nmlnop0iALT  28982  atcvat2i  29374  divnumden2  29692  bnj1542  31053  bnj1253  31211  ptrecube  33539  poimirlem13  33552  ecinn0  34258  llnexchb2  35473  cdlemb3  36211  rencldnfilem  37701  qirropth  37790  binomcxplemfrat  38867  binomcxplemradcnv  38868  odz2prm2pw  41800