Theorem necon3abid 3047

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 3012	. 2 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐴 = 𝐵)
2		necon3abid.1	. . 3 ⊢ (𝜑 → (𝐴 = 𝐵 ↔ 𝜓))
3	2	notbid 320	. 2 ⊢ (𝜑 → (¬ 𝐴 = 𝐵 ↔ ¬ 𝜓))
4	1, 3	syl5bb 285	1 ⊢ (𝜑 → (𝐴 ≠ 𝐵 ↔ ¬ 𝜓))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 208   = wceq 1537   ≠ wne 3011

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 209  df-ne 3012

This theorem is referenced by:  necon3bbid  3048  necon2abid  3053  prnesn  4771  foconst  6584  fndmdif  6793  suppsnop  7825  om00el  8183  oeoa  8204  cardsdom2  9398  mulne0b  11262  crne0  11612  expneg  13422  hashsdom  13727  prprrab  13816  gcdn0gt0  15844  cncongr2  15990  pltval3  17555  mulgnegnn  18216  drngmulne0  19502  lvecvsn0  19859  domnmuln0  20049  mvrf1  20183  connsub  22007  pthaus  22224  xkohaus  22239  bndth  23540  lebnumlem1  23543  dvcobr  24523  dvcnvlem  24553  mdegle0  24652  coemulhi  24825  vieta1lem1  24880  vieta1lem2  24881  aalioulem2  24903  cosne0  25095  atandm3  25437  wilthlem2  25627  issqf  25694  mumullem2  25738  dchrptlem3  25823  lgseisenlem3  25934  brbtwn2  26672  colinearalg  26677  vdn0conngrumgrv2  27954  vdgn1frgrv2  28054  nmlno0lem  28549  nmlnop0iALT  29751  atcvat2i  30143  divnumden2  30515  lindssn  30942  fedgmullem2  31031  bnj1542  32131  bnj1253  32291  ptrecube  34921  poimirlem13  34934  ecinn0  35634  llnexchb2  37032  cdlemb3  37769  rencldnfilem  39504  qirropth  39592  binomcxplemfrat  40768  binomcxplemradcnv  40769  odz2prm2pw  43805