Theorem necon3abid 2961

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 2926	. 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 1540   ≠ wne 2925

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 2926

This theorem is referenced by:  necon3bbid  2962  necon2abid  2967  prneimg2  4809  prnesn  4814  foconst  6755  fndmdif  6980  suppsnop  8118  om00el  8501  oeoa  8522  cardsdom2  9903  mulne0b  11779  crne0  12139  expneg  13994  hashsdom  14306  prprrab  14398  gcdn0gt0  16447  cncongr2  16597  pltval3  18261  mulgnegnn  18981  domnmuln0  20612  drngmulne0  20665  lvecvsn0  21034  mvrf1  21911  connsub  23324  pthaus  23541  xkohaus  23556  bndth  24873  lebnumlem1  24876  dvcobr  25865  dvcobrOLD  25866  dvcnvlem  25896  mdegle0  25998  coemulhi  26175  vieta1lem1  26234  vieta1lem2  26235  aalioulem2  26257  cosne0  26454  atandm3  26804  wilthlem2  26995  issqf  27062  mumullem2  27106  dchrptlem3  27193  lgseisenlem3  27304  mulsne0bd  28112  brbtwn2  28868  colinearalg  28873  vdn0conngrumgrv2  30158  vdgn1frgrv2  30258  nmlno0lem  30755  nmlnop0iALT  31957  atcvat2i  32349  elq2  32769  divnumden2  32773  domnmuln0rd  33224  lindssn  33325  mxidlirredi  33418  mxidlirred  33419  fedgmullem2  33602  minplyirred  33677  cos9thpiminplylem3  33750  bnj1542  34823  bnj1253  34983  ptrecube  37599  poimirlem13  37612  ecinn0  38320  llnexchb2  39848  cdlemb3  40585  aks6d1c2p2  42092  aks6d1c6lem3  42145  fsuppind  42563  rencldnfilem  42793  qirropth  42881  binomcxplemfrat  44324  binomcxplemradcnv  44325  mod2addne  47349  odz2prm2pw  47548