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 1540   ≠ 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  4836  prnesn  4841  foconst  6810  fndmdif  7037  suppsnop  8182  om00el  8593  oeoa  8614  cardsdom2  10007  mulne0b  11883  crne0  12238  expneg  14092  hashsdom  14404  prprrab  14496  gcdn0gt0  16542  cncongr2  16692  pltval3  18354  mulgnegnn  19072  domnmuln0  20674  drngmulne0  20727  lvecvsn0  21075  mvrf1  21951  connsub  23364  pthaus  23581  xkohaus  23596  bndth  24913  lebnumlem1  24916  dvcobr  25906  dvcobrOLD  25907  dvcnvlem  25937  mdegle0  26039  coemulhi  26216  vieta1lem1  26275  vieta1lem2  26276  aalioulem2  26298  cosne0  26495  atandm3  26845  wilthlem2  27036  issqf  27103  mumullem2  27147  dchrptlem3  27234  lgseisenlem3  27345  mulsne0bd  28146  brbtwn2  28889  colinearalg  28894  vdn0conngrumgrv2  30182  vdgn1frgrv2  30282  nmlno0lem  30779  nmlnop0iALT  31981  atcvat2i  32373  elq2  32795  divnumden2  32799  domnmuln0rd  33274  lindssn  33398  mxidlirredi  33491  mxidlirred  33492  fedgmullem2  33675  minplyirred  33750  cos9thpiminplylem3  33823  bnj1542  34893  bnj1253  35053  ptrecube  37649  poimirlem13  37662  ecinn0  38376  llnexchb2  39893  cdlemb3  40630  aks6d1c2p2  42137  aks6d1c6lem3  42190  fsuppind  42580  rencldnfilem  42810  qirropth  42898  binomcxplemfrat  44342  binomcxplemradcnv  44343  odz2prm2pw  47544