Theorem necon3abid 2997

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 2962	. 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 1570   ≠ wne 2961

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 2962

This theorem is used by:  necon3bbid  2998  necon2abid  3003  prneimg2  4825  prnesn  4830  foconst  6814  fndmdif  7044  suppsnop  8183  om00el  8570  oeoa  8592  cardsdom2  9993  mulne0b  11873  crne0  12229  expneg  14125  hashsdom  14437  prprrab  14530  gcdn0gt0  16601  cncongr2  16751  pltval3  18418  mulgnegnn  19181  domnmuln0  20845  drngmulne0  20902  lvecvsn0  21270  mvrf1  22172  connsub  23615  pthaus  23832  xkohaus  23847  bndth  25154  lebnumlem1  25157  dvcobr  26142  dvcnvlem  26172  mdegle0  26271  coemulhi  26448  vieta1lem1  26508  vieta1lem2  26509  aalioulem2  26533  cosne0  26731  atandm3  27080  wilthlem2  27270  issqf  27337  mumullem2  27381  dchrptlem3  27467  lgseisenlem3  27578  mulsne0bd  28416  brbtwn2  29292  colinearalg  29297  vdn0conngrumgrv2  30584  vdgn1frgrv2  30684  nmlno0lem  31182  nmlnop0iALT  32384  atcvat2i  32776  elq2  33193  divnumden2  33197  domnmuln0rd  33628  lindssn  33722  mxidlirredi  33785  mxidlirred  33786  deg1prod  33904  fedgmullem2  34051  minplyirred  34132  cos9thpiminplylem3  34205  bnj1542  35277  bnj1253  35437  ptrecube  38312  poimirlem13  38325  ecinn0  39043  llnexchb2  40684  cdlemb3  41421  aks6d1c2p2  42927  aks6d1c6lem3  42980  fsuppind  43363  rencldnfilem  43588  qirropth  43676  binomcxplemfrat  45102  binomcxplemradcnv  45103  mod2addne  48148  odz2prm2pw  48356