Theorem necon3bbid 2962

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

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

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 2926

This theorem is referenced by:  necon1abid  2963  necon3bid  2969  eldifsn  4740  php  9131  xmullem2  13185  fzdif1  13526  seqcoll2  14390  cnpart  15165  rlimrecl  15505  ncoprmgcdne1b  16579  prmrp  16641  4sqlem17  16891  mrieqvd  17562  mrieqv2d  17563  pltval  18254  latnlemlt  18396  latnle  18397  odnncl  19442  gexnnod  19485  sylow1lem1  19495  slwpss  19509  lssnle  19571  nzrunit  20427  imadrhmcl  20700  lspsnne1  21042  cnsubrg  21352  psrridm  21888  mhpmulcl  22052  cmpfi  23311  hausdiag  23548  txhaus  23550  isusp  24165  recld2  24719  metdseq0  24759  i1f1lem  25606  aaliou2b  26265  dvloglem  26573  logf1o2  26575  lgsne0  27262  lgsqr  27278  2sqlem7  27351  ostth3  27565  tglngne  28513  tgelrnln  28593  eucrct2eupth  30207  norm1exi  31212  atnemeq0  32339  opeldifid  32561  arginv  32704  sgnneg  32791  unitnz  33189  isdrng4  33244  pridln1  33390  mxidln1  33413  ssmxidllem  33420  rprmnz  33467  ply1unit  33520  ply1dg3rt0irred  33527  constrrtll  33697  qtophaus  33802  ordtconnlem1  33890  elzrhunit  33943  subfacp1lem6  35157  maxidln1  38023  smprngopr  38031  lsatnem0  39023  atncmp  39290  atncvrN  39293  cdlema2N  39771  lhpmatb  40010  lhpat3  40025  cdleme3  40216  cdleme7  40228  cdlemg27b  40675  dvh2dimatN  41419  dvh2dim  41424  dochexmidlem1  41439  dochfln0  41456  dvrelog2b  42039  aks6d1c2p2  42092  hashscontpow  42095  rspcsbnea  42104  nna4b4nsq  42633