Theorem necon3abid 2978

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   = wceq 1542   ≠ wne 2941

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 206  df-ne 2942

This theorem is referenced by:  necon3bbid  2979  necon2abid  2984  prnesn  4861  foconst  6821  fndmdif  7044  suppsnop  8163  om00el  8576  oeoa  8597  cardsdom2  9983  mulne0b  11855  crne0  12205  expneg  14035  hashsdom  14341  prprrab  14434  gcdn0gt0  16459  cncongr2  16605  pltval3  18292  mulgnegnn  18964  drngmulne0  20387  lvecvsn0  20722  domnmuln0  20914  mvrf1  21545  connsub  22925  pthaus  23142  xkohaus  23157  bndth  24474  lebnumlem1  24477  dvcobr  25463  dvcnvlem  25493  mdegle0  25595  coemulhi  25768  vieta1lem1  25823  vieta1lem2  25824  aalioulem2  25846  cosne0  26038  atandm3  26383  wilthlem2  26573  issqf  26640  mumullem2  26684  dchrptlem3  26769  lgseisenlem3  26880  brbtwn2  28163  colinearalg  28168  vdn0conngrumgrv2  29449  vdgn1frgrv2  29549  nmlno0lem  30046  nmlnop0iALT  31248  atcvat2i  31640  divnumden2  32024  lindssn  32494  mxidlirredi  32587  mxidlirred  32588  fedgmullem2  32715  minplyirred  32770  bnj1542  33868  bnj1253  34028  gg-dvcobr  35176  ptrecube  36488  poimirlem13  36501  ecinn0  37222  llnexchb2  38740  cdlemb3  39477  aks6d1c2p2  40957  fsuppind  41162  rencldnfilem  41558  qirropth  41646  binomcxplemfrat  43110  binomcxplemradcnv  43111  odz2prm2pw  46231