Theorem necon3abid 3052

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 3017	. 2 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐴 = 𝐵)
2		necon3abid.1	. . 3 ⊢ (𝜑 → (𝐴 = 𝐵 ↔ 𝜓))
3	2	notbid 320	. 2 ⊢ (𝜑 → (¬ 𝐴 = 𝐵 ↔ ¬ 𝜓))
4	1, 3	syl5bb 285	1 ⊢ (𝜑 → (𝐴 ≠ 𝐵 ↔ ¬ 𝜓))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 208   = wceq 1537   ≠ wne 3016

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 209  df-ne 3017

This theorem is referenced by:  necon3bbid  3053  necon2abid  3058  prnesn  4790  foconst  6603  fndmdif  6812  suppsnop  7844  om00el  8202  oeoa  8223  cardsdom2  9417  mulne0b  11281  crne0  11631  expneg  13438  hashsdom  13743  prprrab  13832  gcdn0gt0  15866  cncongr2  16012  pltval3  17577  mulgnegnn  18238  drngmulne0  19524  lvecvsn0  19881  domnmuln0  20071  mvrf1  20205  connsub  22029  pthaus  22246  xkohaus  22261  bndth  23562  lebnumlem1  23565  dvcobr  24543  dvcnvlem  24573  mdegle0  24671  coemulhi  24844  vieta1lem1  24899  vieta1lem2  24900  aalioulem2  24922  cosne0  25114  atandm3  25456  wilthlem2  25646  issqf  25713  mumullem2  25757  dchrptlem3  25842  lgseisenlem3  25953  brbtwn2  26691  colinearalg  26696  vdn0conngrumgrv2  27975  vdgn1frgrv2  28075  nmlno0lem  28570  nmlnop0iALT  29772  atcvat2i  30164  divnumden2  30534  lindssn  30939  fedgmullem2  31026  bnj1542  32129  bnj1253  32289  ptrecube  34907  poimirlem13  34920  ecinn0  35622  llnexchb2  37020  cdlemb3  37757  rencldnfilem  39437  qirropth  39525  binomcxplemfrat  40703  binomcxplemradcnv  40704  odz2prm2pw  43745