Theorem necon3abid 2971

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 207   = wceq 1547   ≠ wne 2935

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 208  df-ne 2936

This theorem is referenced by:  necon3bbid  2972  necon2abid  2977  prneimg2  4793  prnesn  4798  foconst  6761  fndmdif  6990  suppsnop  8125  om00el  8508  oeoa  8530  cardsdom2  9910  mulne0b  11789  crne0  12150  expneg  14029  hashsdom  14341  prprrab  14433  gcdn0gt0  16485  cncongr2  16635  pltval3  18301  mulgnegnn  19058  domnmuln0  20688  drngmulne0  20741  lvecvsn0  21109  mvrf1  21967  connsub  23411  pthaus  23628  xkohaus  23643  bndth  24950  lebnumlem1  24953  dvcobr  25938  dvcnvlem  25968  mdegle0  26067  coemulhi  26244  vieta1lem1  26301  vieta1lem2  26302  aalioulem2  26324  cosne0  26518  atandm3  26867  wilthlem2  27057  issqf  27124  mumullem2  27168  dchrptlem3  27254  lgseisenlem3  27365  mulsne0bd  28203  brbtwn2  28999  colinearalg  29004  vdn0conngrumgrv2  30291  vdgn1frgrv2  30391  nmlno0lem  30889  nmlnop0iALT  32091  atcvat2i  32483  elq2  32911  divnumden2  32915  domnmuln0rd  33362  lindssn  33468  mxidlirredi  33561  mxidlirred  33562  deg1prod  33673  fedgmullem2  33821  minplyirred  33902  cos9thpiminplylem3  33975  bnj1542  35046  bnj1253  35206  ptrecube  37994  poimirlem13  38007  ecinn0  38727  llnexchb2  40368  cdlemb3  41105  aks6d1c2p2  42611  aks6d1c6lem3  42664  fsuppind  43047  rencldnfilem  43272  qirropth  43360  binomcxplemfrat  44802  binomcxplemradcnv  44803  mod2addne  47840  odz2prm2pw  48048