Theorem necon3bbid 2975

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 223	. . 3 ⊢ (𝜑 → (𝐴 = 𝐵 ↔ 𝜓))
3	2	necon3abid 2974	. 2 ⊢ (𝜑 → (𝐴 ≠ 𝐵 ↔ ¬ 𝜓))
4	3	bicomd 223	1 ⊢ (𝜑 → (¬ 𝜓 ↔ 𝐴 ≠ 𝐵))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   = wceq 1536   ≠ wne 2937

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 207  df-ne 2938

This theorem is referenced by:  necon1abid  2976  necon3bid  2982  eldifsn  4790  php  9244  phpOLD  9256  xmullem2  13303  fzdif1  13641  seqcoll2  14500  cnpart  15275  rlimrecl  15612  ncoprmgcdne1b  16683  prmrp  16745  4sqlem17  16994  mrieqvd  17682  mrieqv2d  17683  pltval  18389  latnlemlt  18529  latnle  18530  odnncl  19577  gexnnod  19620  sylow1lem1  19630  slwpss  19644  lssnle  19706  nzrunit  20540  imadrhmcl  20814  lspsnne1  21136  cnsubrg  21462  psrridm  22000  mhpmulcl  22170  cmpfi  23431  hausdiag  23668  txhaus  23670  isusp  24285  recld2  24849  metdseq0  24889  i1f1lem  25737  aaliou2b  26397  dvloglem  26704  logf1o2  26706  lgsne0  27393  lgsqr  27409  2sqlem7  27482  ostth3  27696  tglngne  28572  tgelrnln  28652  eucrct2eupth  30273  norm1exi  31278  atnemeq0  32405  opeldifid  32618  unitnz  33228  isdrng4  33278  pridln1  33450  mxidln1  33473  ssmxidllem  33480  rprmnz  33527  ply1unit  33579  ply1dg3rt0irred  33586  constrrtll  33736  qtophaus  33796  ordtconnlem1  33884  elzrhunit  33939  sgnneg  34521  subfacp1lem6  35169  maxidln1  38030  smprngopr  38038  lsatnem0  39026  atncmp  39293  atncvrN  39296  cdlema2N  39774  lhpmatb  40013  lhpat3  40028  cdleme3  40219  cdleme7  40231  cdlemg27b  40678  dvh2dimatN  41422  dvh2dim  41427  dochexmidlem1  41442  dochfln0  41459  dvrelog2b  42047  aks6d1c2p2  42100  hashscontpow  42103  rspcsbnea  42112  nna4b4nsq  42646