Theorem necon3bbid 2831

Description: Deduction from equality to inequality. (Contributed by NM, 2-Jun-2007.)

Hypothesis

Ref	Expression
necon3bbid.1	⊢ (𝜑 → (𝜓 ↔ 𝐴 = 𝐵))

Assertion

Ref	Expression
necon3bbid	⊢ (𝜑 → (¬ 𝜓 ↔ 𝐴 ≠ 𝐵))

Proof of Theorem necon3bbid

Step	Hyp	Ref	Expression
1		necon3bbid.1	. . . 4 ⊢ (𝜑 → (𝜓 ↔ 𝐴 = 𝐵))
2	1	bicomd 213	. . 3 ⊢ (𝜑 → (𝐴 = 𝐵 ↔ 𝜓))
3	2	necon3abid 2830	. 2 ⊢ (𝜑 → (𝐴 ≠ 𝐵 ↔ ¬ 𝜓))
4	3	bicomd 213	1 ⊢ (𝜑 → (¬ 𝜓 ↔ 𝐴 ≠ 𝐵))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 196   = wceq 1483   ≠ wne 2794

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 197  df-ne 2795

This theorem is referenced by:  necon1abid  2832  necon3bid  2838  eldifsn  4317  php  8144  xmullem2  12095  seqcoll2  13249  cnpart  13980  rlimrecl  14311  ncoprmgcdne1b  15363  prmrp  15424  4sqlem17  15665  mrieqvd  16298  mrieqv2d  16299  pltval  16960  latnlemlt  17084  latnle  17085  odnncl  17964  gexnnod  18003  sylow1lem1  18013  slwpss  18027  lssnle  18087  lspsnne1  19117  nzrunit  19267  psrridm  19404  cnsubrg  19806  cmpfi  21211  hausdiag  21448  txhaus  21450  isusp  22065  recld2  22617  metdseq0  22657  i1f1lem  23456  aaliou2b  24096  dvloglem  24394  logf1o2  24396  lgsne0  25060  lgsqr  25076  2sqlem7  25149  ostth3  25327  tglngne  25445  tgelrnln  25525  eucrct2eupth  27105  norm1exi  28107  atnemeq0  29236  opeldifid  29412  qtophaus  29903  ordtconnlem1  29970  elzrhunit  30023  sgnneg  30602  subfacp1lem6  31167  maxidln1  33843  smprngopr  33851  lsatnem0  34332  atncmp  34599  atncvrN  34602  cdlema2N  35078  lhpmatb  35317  lhpat3  35332  cdleme3  35524  cdleme7  35536  cdlemg27b  35984  dvh2dimatN  36729  dvh2dim  36734  dochexmidlem1  36749  dochfln0  36766