Theorem necon3abid 2968

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 2933	. 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 1541   ≠ wne 2932

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 2933

This theorem is referenced by:  necon3bbid  2969  necon2abid  2974  prneimg2  4811  prnesn  4816  foconst  6761  fndmdif  6987  suppsnop  8120  om00el  8503  oeoa  8525  cardsdom2  9900  mulne0b  11778  crne0  12138  expneg  13992  hashsdom  14304  prprrab  14396  gcdn0gt0  16445  cncongr2  16595  pltval3  18260  mulgnegnn  19014  domnmuln0  20642  drngmulne0  20695  lvecvsn0  21064  mvrf1  21941  connsub  23365  pthaus  23582  xkohaus  23597  bndth  24913  lebnumlem1  24916  dvcobr  25905  dvcobrOLD  25906  dvcnvlem  25936  mdegle0  26038  coemulhi  26215  vieta1lem1  26274  vieta1lem2  26275  aalioulem2  26297  cosne0  26494  atandm3  26844  wilthlem2  27035  issqf  27102  mumullem2  27146  dchrptlem3  27233  lgseisenlem3  27344  mulsne0bd  28182  brbtwn2  28978  colinearalg  28983  vdn0conngrumgrv2  30271  vdgn1frgrv2  30371  nmlno0lem  30868  nmlnop0iALT  32070  atcvat2i  32462  elq2  32892  divnumden2  32896  domnmuln0rd  33356  lindssn  33459  mxidlirredi  33552  mxidlirred  33553  deg1prod  33664  fedgmullem2  33787  minplyirred  33868  cos9thpiminplylem3  33941  bnj1542  35013  bnj1253  35173  ptrecube  37817  poimirlem13  37830  ecinn0  38542  llnexchb2  40125  cdlemb3  40862  aks6d1c2p2  42369  aks6d1c6lem3  42422  fsuppind  42829  rencldnfilem  43058  qirropth  43146  binomcxplemfrat  44588  binomcxplemradcnv  44589  mod2addne  47606  odz2prm2pw  47805