Theorem necon3abid 2965

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 2930	. 2 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐴 = 𝐵)
2		necon3abid.1	. . 3 ⊢ (𝜑 → (𝐴 = 𝐵 ↔ 𝜓))
3	2	notbid 318	. 2 ⊢ (𝜑 → (¬ 𝐴 = 𝐵 ↔ ¬ 𝜓))
4	1, 3	bitrid 283	1 ⊢ (𝜑 → (𝐴 ≠ 𝐵 ↔ ¬ 𝜓))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   = wceq 1541   ≠ wne 2929

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 207  df-ne 2930

This theorem is referenced by:  necon3bbid  2966  necon2abid  2971  prneimg2  4806  prnesn  4811  foconst  6755  fndmdif  6981  suppsnop  8114  om00el  8497  oeoa  8518  cardsdom2  9888  mulne0b  11765  crne0  12125  expneg  13978  hashsdom  14290  prprrab  14382  gcdn0gt0  16431  cncongr2  16581  pltval3  18245  mulgnegnn  18999  domnmuln0  20626  drngmulne0  20679  lvecvsn0  21048  mvrf1  21924  connsub  23337  pthaus  23554  xkohaus  23569  bndth  24885  lebnumlem1  24888  dvcobr  25877  dvcobrOLD  25878  dvcnvlem  25908  mdegle0  26010  coemulhi  26187  vieta1lem1  26246  vieta1lem2  26247  aalioulem2  26269  cosne0  26466  atandm3  26816  wilthlem2  27007  issqf  27074  mumullem2  27118  dchrptlem3  27205  lgseisenlem3  27316  mulsne0bd  28126  brbtwn2  28885  colinearalg  28890  vdn0conngrumgrv2  30178  vdgn1frgrv2  30278  nmlno0lem  30775  nmlnop0iALT  31977  atcvat2i  32369  elq2  32799  divnumden2  32803  domnmuln0rd  33248  lindssn  33350  mxidlirredi  33443  mxidlirred  33444  fedgmullem2  33664  minplyirred  33745  cos9thpiminplylem3  33818  bnj1542  34890  bnj1253  35050  ptrecube  37681  poimirlem13  37694  ecinn0  38406  llnexchb2  39989  cdlemb3  40726  aks6d1c2p2  42233  aks6d1c6lem3  42286  fsuppind  42709  rencldnfilem  42938  qirropth  43026  binomcxplemfrat  44469  binomcxplemradcnv  44470  mod2addne  47489  odz2prm2pw  47688