Theorem necon3bbid 3053

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 225	. . 3 ⊢ (𝜑 → (𝐴 = 𝐵 ↔ 𝜓))
3	2	necon3abid 3052	. 2 ⊢ (𝜑 → (𝐴 ≠ 𝐵 ↔ ¬ 𝜓))
4	3	bicomd 225	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:  necon1abid  3054  necon3bid  3060  eldifsn  4719  php  8701  xmullem2  12659  seqcoll2  13824  cnpart  14599  rlimrecl  14937  ncoprmgcdne1b  15994  prmrp  16056  4sqlem17  16297  mrieqvd  16909  mrieqv2d  16910  pltval  17570  latnlemlt  17694  latnle  17695  odnncl  18673  gexnnod  18713  sylow1lem1  18723  slwpss  18737  lssnle  18800  lspsnne1  19889  nzrunit  20040  psrridm  20184  cnsubrg  20605  cmpfi  22016  hausdiag  22253  txhaus  22255  isusp  22870  recld2  23422  metdseq0  23462  i1f1lem  24290  aaliou2b  24930  dvloglem  25231  logf1o2  25233  lgsne0  25911  lgsqr  25927  2sqlem7  26000  ostth3  26214  tglngne  26336  tgelrnln  26416  eucrct2eupth  28024  norm1exi  29027  atnemeq0  30154  opeldifid  30349  pridln1  30959  mxidln1  30975  ssmxidllem  30978  qtophaus  31100  ordtconnlem1  31167  elzrhunit  31220  sgnneg  31798  subfacp1lem6  32432  maxidln1  35337  smprngopr  35345  lsatnem0  36196  atncmp  36463  atncvrN  36466  cdlema2N  36943  lhpmatb  37182  lhpat3  37197  cdleme3  37388  cdleme7  37400  cdlemg27b  37847  dvh2dimatN  38591  dvh2dim  38596  dochexmidlem1  38611  dochfln0  38628