Theorem necon3abid 2992

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 2957	. 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 2956

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 2957

This theorem is used by:  necon3bbid  2993  necon2abid  2998  prneimg2  4815  prnesn  4820  foconst  6812  fndmdif  7042  suppsnop  8196  tz7.48lem  8451  om00el  8585  oeoa  8607  cardsdom2  10070  mulne0b  11958  crne0  12314  expneg  14213  hashsdom  14526  prprrab  14619  gcdn0gt0  16691  cncongr2  16844  pltval3  18512  mulgnegnn  19295  domnmuln0  20962  drngmulne0  21020  lvecvsn0  21388  mvrf1  22294  connsub  23740  pthaus  23958  xkohaus  23973  bndth  25280  lebnumlem1  25283  dvcobr  26267  dvcnvlem  26297  mdegle0  26396  coemulhi  26574  vieta1lem1  26634  vieta1lem2  26635  aalioulem2  26661  cosne0  26858  atandm3  27207  wilthlem2  27397  issqf  27464  mumullem2  27508  dchrptlem3  27594  lgseisenlem3  27705  mulsne0bd  28573  brbtwn2  29484  colinearalg  29489  vdn0conngrumgrv2  30798  vdgn1frgrv2  30898  nmlno0lem  31396  nmlnop0iALT  32598  atcvat2i  32990  elq2  33404  divnumden2  33408  domnmuln0rd  33839  lindssn  33934  mxidlirredi  33997  mxidlirred  33998  deg1prod  34116  fedgmullem2  34263  minplyirred  34344  cos9thpiminplylem3  34417  bnj1542  35488  bnj1253  35648  ptrecube  38540  poimirlem13  38553  ecinn0  39287  llnexchb2  40928  cdlemb3  41665  aks6d1c2p2  43171  aks6d1c6lem3  43224  fsuppind  43620  rencldnfilem  43828  qirropth  43916  binomcxplemfrat  45336  binomcxplemradcnv  45337  mod2addne  48441  odz2prm2pw  48649