Theorem necon3abid 2983

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 2947	. 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 1537   ≠ wne 2946

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 2947

This theorem is referenced by:  necon3bbid  2984  necon2abid  2989  prnesn  4884  foconst  6849  fndmdif  7075  suppsnop  8219  om00el  8632  oeoa  8653  cardsdom2  10057  mulne0b  11931  crne0  12286  expneg  14120  hashsdom  14430  prprrab  14522  gcdn0gt0  16564  cncongr2  16715  pltval3  18409  mulgnegnn  19124  domnmuln0  20731  drngmulne0  20784  lvecvsn0  21134  mvrf1  22029  connsub  23450  pthaus  23667  xkohaus  23682  bndth  25009  lebnumlem1  25012  dvcobr  26003  dvcobrOLD  26004  dvcnvlem  26034  mdegle0  26136  coemulhi  26313  vieta1lem1  26370  vieta1lem2  26371  aalioulem2  26393  cosne0  26589  atandm3  26939  wilthlem2  27130  issqf  27197  mumullem2  27241  dchrptlem3  27328  lgseisenlem3  27439  mulsne0bd  28230  brbtwn2  28938  colinearalg  28943  vdn0conngrumgrv2  30228  vdgn1frgrv2  30328  nmlno0lem  30825  nmlnop0iALT  32027  atcvat2i  32419  divnumden2  32819  domnmuln0rd  33246  lindssn  33371  mxidlirredi  33464  mxidlirred  33465  fedgmullem2  33643  minplyirred  33704  bnj1542  34833  bnj1253  34993  ptrecube  37580  poimirlem13  37593  ecinn0  38309  llnexchb2  39826  cdlemb3  40563  aks6d1c2p2  42076  aks6d1c6lem3  42129  fsuppind  42545  rencldnfilem  42776  qirropth  42864  binomcxplemfrat  44320  binomcxplemradcnv  44321  odz2prm2pw  47437