Theorem necon3abid 2977

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 2941	. 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 2940

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 2941

This theorem is referenced by:  necon3bbid  2978  necon2abid  2983  prneimg2  4855  prnesn  4860  foconst  6835  fndmdif  7062  suppsnop  8203  om00el  8614  oeoa  8635  cardsdom2  10028  mulne0b  11904  crne0  12259  expneg  14110  hashsdom  14420  prprrab  14512  gcdn0gt0  16555  cncongr2  16705  pltval3  18384  mulgnegnn  19102  domnmuln0  20709  drngmulne0  20762  lvecvsn0  21111  mvrf1  22006  connsub  23429  pthaus  23646  xkohaus  23661  bndth  24990  lebnumlem1  24993  dvcobr  25983  dvcobrOLD  25984  dvcnvlem  26014  mdegle0  26116  coemulhi  26293  vieta1lem1  26352  vieta1lem2  26353  aalioulem2  26375  cosne0  26571  atandm3  26921  wilthlem2  27112  issqf  27179  mumullem2  27223  dchrptlem3  27310  lgseisenlem3  27421  mulsne0bd  28212  brbtwn2  28920  colinearalg  28925  vdn0conngrumgrv2  30215  vdgn1frgrv2  30315  nmlno0lem  30812  nmlnop0iALT  32014  atcvat2i  32406  divnumden2  32817  domnmuln0rd  33278  lindssn  33406  mxidlirredi  33499  mxidlirred  33500  fedgmullem2  33681  minplyirred  33754  bnj1542  34871  bnj1253  35031  ptrecube  37627  poimirlem13  37640  ecinn0  38354  llnexchb2  39871  cdlemb3  40608  aks6d1c2p2  42120  aks6d1c6lem3  42173  fsuppind  42600  rencldnfilem  42831  qirropth  42919  binomcxplemfrat  44370  binomcxplemradcnv  44371  odz2prm2pw  47550