Theorem necon3abid 2991

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   = wceq 1569   ≠ wne 2955

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-ne 2956

This theorem is used by:  necon3bbid  2992  necon2abid  2997  prneimg2  4809  prnesn  4814  foconst  6812  fndmdif  7042  suppsnop  8199  tz7.48lem  8454  om00el  8588  oeoa  8610  cardsdom2  10073  mulne0b  11961  crne0  12317  expneg  14216  hashsdom  14529  prprrab  14622  gcdn0gt0  16696  cncongr2  16849  pltval3  18517  mulgnegnn  19300  domnmuln0  20967  drngmulne0  21025  lvecvsn0  21393  mvrf1  22299  connsub  23745  pthaus  23963  xkohaus  23978  bndth  25285  lebnumlem1  25288  dvcobr  26272  dvcnvlem  26302  mdegle0  26401  coemulhi  26579  vieta1lem1  26639  vieta1lem2  26640  aalioulem2  26666  cosne0  26863  atandm3  27212  wilthlem2  27402  issqf  27469  mumullem2  27513  dchrptlem3  27599  lgseisenlem3  27710  mulsne0bd  28578  brbtwn2  29489  colinearalg  29494  vdn0conngrumgrv2  30803  vdgn1frgrv2  30903  nmlno0lem  31401  nmlnop0iALT  32603  atcvat2i  32995  elq2  33450  divnumden2  33454  domnmuln0rd  33885  lindssn  33980  mxidlirredi  34043  mxidlirred  34044  deg1prod  34162  fedgmullem2  34309  minplyirred  34390  cos9thpiminplylem3  34463  bnj1542  35534  bnj1253  35694  ptrecube  38632  poimirlem13  38645  ecinn0  39379  llnexchb2  41020  cdlemb3  41757  aks6d1c2p2  43263  aks6d1c6lem3  43316  fsuppind  43712  rencldnfilem  43921  qirropth  44009  binomcxplemfrat  45429  binomcxplemradcnv  45430  mod2addne  48534  odz2prm2pw  48742