Theorem necon3abid 2969

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 2934	. 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 1542   ≠ wne 2933

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 2934

This theorem is referenced by:  necon3bbid  2970  necon2abid  2975  prneimg2  4813  prnesn  4818  foconst  6769  fndmdif  6996  suppsnop  8130  om00el  8513  oeoa  8535  cardsdom2  9912  mulne0b  11790  crne0  12150  expneg  14004  hashsdom  14316  prprrab  14408  gcdn0gt0  16457  cncongr2  16607  pltval3  18272  mulgnegnn  19026  domnmuln0  20654  drngmulne0  20707  lvecvsn0  21076  mvrf1  21953  connsub  23377  pthaus  23594  xkohaus  23609  bndth  24925  lebnumlem1  24928  dvcobr  25917  dvcobrOLD  25918  dvcnvlem  25948  mdegle0  26050  coemulhi  26227  vieta1lem1  26286  vieta1lem2  26287  aalioulem2  26309  cosne0  26506  atandm3  26856  wilthlem2  27047  issqf  27114  mumullem2  27158  dchrptlem3  27245  lgseisenlem3  27356  mulsne0bd  28194  brbtwn2  28990  colinearalg  28995  vdn0conngrumgrv2  30283  vdgn1frgrv2  30383  nmlno0lem  30880  nmlnop0iALT  32082  atcvat2i  32474  elq2  32902  divnumden2  32906  domnmuln0rd  33367  lindssn  33470  mxidlirredi  33563  mxidlirred  33564  deg1prod  33675  fedgmullem2  33807  minplyirred  33888  cos9thpiminplylem3  33961  bnj1542  35032  bnj1253  35192  ptrecube  37865  poimirlem13  37878  ecinn0  38598  llnexchb2  40239  cdlemb3  40976  aks6d1c2p2  42483  aks6d1c6lem3  42536  fsuppind  42942  rencldnfilem  43171  qirropth  43259  binomcxplemfrat  44701  binomcxplemradcnv  44702  mod2addne  47718  odz2prm2pw  47917